HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem xpex 3250
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23.
Hypotheses
Ref Expression
xpex.1 |- A e. V
xpex.2 |- B e. V
Assertion
Ref Expression
xpex |- (A X. B) e. V
Proof of Theorem xpex
StepHypRef Expression
1 xpex.1 . 2 |- A e. V
2 xpex.2 . 2 |- B e. V
3 xpexg 3249 . 2 |- ((A e. V /\ B e. V) -> (A X. B) e. V)
41, 2, 3mp2an 695 1 |- (A X. B) e. V
Colors of variables: wff set class
Syntax hints:   e. wcel 955  Vcvv 1802   X. cxp 3158
This theorem is referenced by:  oprabex 4004  oprabex3 4007  oprvalex 4026  elpm 4320  map0 4328  map1 4411  xpsnen 4415  endisj 4417  xpcomen 4419  xpassen 4421  xpdom2 4422  xpdom3 4425  xpen 4468  mapxpen 4475  xpmapenlem5 4480  rankxpl 4682  rankxplim 4684  rankxplim2 4685  rankxplim3 4686  rankxpsuc 4687  aceq3 4705  aceq5lem2 4708  aceq5lem3 4709  weth 4759  unxpdomlem 4815  unxpdom2 4817  sucxpdom 4818  uncdadom 4893  cdaassen 4902  xpcdaen 4903  mapcdaen 4904  cdadom1 4905  enqex 5020  nqex 5021  enrex 5150  srex 5151  axcnex 5239  addex 5289  mulex 5290  exp1t 6505  expp1t 6506  serz0 6991  serzcmp0 6993  climconst2 7032  climconst3 7033  climuz0 7045  climaddc1 7054  climmulc2 7065  climsubc2 7067  climcmpc1 7075  iserzcmp0 7079  ser1const 7107  acdc3lem 7428  acdclem 7436  xpnnen 7441  xpomen 7442  qnnen 7446  ruclem9 7461  infxpidmlem1 7495  infxpidmlem9 7503  infxpidmlem10 7504  infxpidmlem12 7506  infmap1 7516  iunctb 7517  infmap2lem2 7522  infmap2 7523  ismeti 7741  metxp 7774  lmclim 7898  metelcls 7900  bcthlem12 7944  bcthlem15 7947  bcthlem30 7962  isgrpi 7976  isgrp2i 8011  vcoprne 8136  sspval 8316  0ofval 8379  ajfval 8400  hvmulex 8802  hlim0 9026  hlimcau 9028  hlimuni 9030
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-opab 2657  df-xp 3174  df-rel 3175
Copyright terms: Public domain