MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpex Unicode version

Theorem xpex 4708
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
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 4707 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 656 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2727    X. cxp 4578
This theorem is referenced by:  oprabex  5813  oprabex3  5814  fnpm  6666  mapsnf1o2  6701  ixpsnf1o  6742  xpsnen  6831  endisj  6834  xpcomen  6838  xpassen  6841  xpmapenlem  6913  mapunen  6915  unxpdomlem3  6954  hartogslem1  7141  rankxpl  7431  rankxplim  7433  rankxplim2  7434  rankxplim3  7435  rankxpsuc  7436  r0weon  7524  infxpenlem  7525  infxpenc2lem2  7531  dfac3  7632  dfac5lem2  7635  dfac5lem3  7636  dfac5lem4  7637  cdafn  7679  unctb  7715  axcc2lem  7946  axdc3lem  7960  axdc4lem  7965  enqex  8426  nqex  8427  enrex  8572  axcnex  8649  zexALT  9921  cnexALT  10229  addex  10231  mulex  10232  ixxex  10545  shftfval  11442  climconst2  11899  xpnnenOLD  12362  cpnnen  12381  ruclem13  12394  cnso  12399  prdsval  13229  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  prdsle  13235  prdsds  13237  prdshom  13240  prdsco  13241  fnmrc  13381  mrcfval  13382  mreacs  13404  comfffval  13445  oppccofval  13463  sectfval  13498  brssc  13535  sscpwex  13536  isssc  13541  isfunc  13582  isfuncd  13583  idfu2nd  13595  idfu1st  13597  idfucl  13599  wunfunc  13617  fuccofval  13677  homafval  13705  homaf  13706  homaval  13707  coapm  13747  catccofval  13776  catcfuccl  13785  fnxpc  13794  xpcval  13795  xpcbas  13796  xpchom  13798  xpccofval  13800  1stfval  13809  2ndfval  13812  1stfcl  13815  2ndfcl  13816  catcxpccl  13825  evlf2  13836  evlf1  13838  evlfcl  13840  hof1fval  13871  hof2fval  13873  hofcl  13877  ipoval  14101  letsr  14184  plusffval  14214  frmdplusg  14311  eqgfval  14500  efglem  14860  efgval  14861  scaffval  15480  psrplusg  15958  ltbval  16045  opsrle  16049  evlslem2  16081  cnfldds  16221  xrsadd  16223  xrsmul  16224  xrsle  16226  xrsds  16246  znle  16322  ipffval  16384  pjfval  16438  2ndcctbss  17013  txuni2  17092  txbas  17094  eltx  17095  txcnp  17146  txcnmpt  17150  txrest  17157  txlm  17174  tx1stc  17176  tx2ndc  17177  txkgen  17178  txflf  17533  distgp  17614  indistgp  17615  ishtpy  18302  isphtpc  18324  elovolm  18666  elovolmr  18667  ovolmge0  18668  ovolgelb  18671  ovolunlem1a  18687  ovolunlem1  18688  ovoliunlem1  18693  ovoliunlem2  18694  ovolshftlem2  18701  ovolicc2  18713  ioombl1  18751  dyadmbl  18787  vitali  18800  mbfimaopnlem  18842  dvfval  19079  evlssca  19238  mpfind  19260  pf1ind  19270  plyeq0lem  19424  taylfval  19570  ulmval  19591  dmarea  20084  dchrplusg  20318  isgrpoi  20695  vcoprne  20965  sspval  21129  0ofval  21195  ajfval  21217  hvmulex  21421  cvmlift2lem9  23013  iseupa  23052  brimg  23650  brrestrict  23661  axlowdimlem15  23758  axlowdim  23763  colinearex  23857  nZdef  24346  issubcat  25011  heiborlem3  25703  rrnval  25717  ismrer1  25728  mzpincl  25978  pellexlem3  26082  pellexlem4  26083  pellexlem5  26084  aomclem6  26322  lcvfbr  27899  cmtfvalN  28089  cvrfval  28147  dvhvbase  29966  dvhfvadd  29970  dvhfvsca  29979  dibval  30021  dibfna  30033  dicval  30055  hdmap1fval  30676
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-rex 2514  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-opab 3975  df-xp 4594
  Copyright terms: Public domain W3C validator