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

Theorem xpex 4789
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 4788 . 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 2763    X. cxp 4659
This theorem is referenced by:  oprabex  5895  oprabex3  5896  fnpm  6748  mapsnf1o2  6783  ixpsnf1o  6824  xpsnen  6914  endisj  6917  xpcomen  6921  xpassen  6924  xpmapenlem  6996  mapunen  6998  unxpdomlem3  7037  hartogslem1  7225  rankxpl  7515  rankxplim  7517  rankxplim2  7518  rankxplim3  7519  rankxpsuc  7520  r0weon  7608  infxpenlem  7609  infxpenc2lem2  7615  dfac3  7716  dfac5lem2  7719  dfac5lem3  7720  dfac5lem4  7721  cdafn  7763  unctb  7799  axcc2lem  8030  axdc3lem  8044  axdc4lem  8049  enqex  8514  nqex  8515  enrex  8660  axcnex  8737  zexALT  10010  cnexALT  10318  addex  10320  mulex  10321  ixxex  10634  shftfval  11531  climconst2  11988  xpnnenOLD  12451  cpnnen  12470  ruclem13  12483  cnso  12488  prdsval  13318  prdsplusg  13321  prdsmulr  13322  prdsvsca  13323  prdsle  13324  prdsds  13326  prdshom  13329  prdsco  13330  fnmrc  13472  mrcfval  13473  mreacs  13523  comfffval  13564  oppccofval  13582  sectfval  13617  brssc  13654  sscpwex  13655  isssc  13660  isfunc  13701  isfuncd  13702  idfu2nd  13714  idfu1st  13716  idfucl  13718  wunfunc  13736  fuccofval  13796  homafval  13824  homaf  13825  homaval  13826  coapm  13866  catccofval  13895  catcfuccl  13904  fnxpc  13913  xpcval  13914  xpcbas  13915  xpchom  13917  xpccofval  13919  1stfval  13928  2ndfval  13931  1stfcl  13934  2ndfcl  13935  catcxpccl  13944  evlf2  13955  evlf1  13957  evlfcl  13959  hof1fval  13990  hof2fval  13992  hofcl  13996  ipoval  14220  letsr  14312  plusffval  14342  frmdplusg  14439  eqgfval  14628  efglem  14988  efgval  14989  scaffval  15608  psrplusg  16089  ltbval  16176  opsrle  16180  evlslem2  16212  cnfldds  16352  xrsadd  16354  xrsmul  16355  xrsle  16357  xrsds  16377  znle  16453  ipffval  16515  pjfval  16569  2ndcctbss  17144  txuni2  17223  txbas  17225  eltx  17226  txcnp  17277  txcnmpt  17281  txrest  17288  txlm  17305  tx1stc  17307  tx2ndc  17308  txkgen  17309  txflf  17664  distgp  17745  indistgp  17746  ishtpy  18433  isphtpc  18455  elovolm  18797  elovolmr  18798  ovolmge0  18799  ovolgelb  18802  ovolunlem1a  18818  ovolunlem1  18819  ovoliunlem1  18824  ovoliunlem2  18825  ovolshftlem2  18832  ovolicc2  18844  ioombl1  18882  dyadmbl  18918  vitali  18931  mbfimaopnlem  18973  dvfval  19210  evlssca  19369  mpfind  19391  pf1ind  19401  plyeq0lem  19555  taylfval  19701  ulmval  19722  dmarea  20215  dchrplusg  20449  isgrpoi  20826  vcoprne  21096  sspval  21260  0ofval  21326  ajfval  21348  hvmulex  21552  cvmlift2lem9  23215  iseupa  23254  brimg  23852  brrestrict  23863  axlowdimlem15  23960  axlowdim  23965  colinearex  24059  nZdef  24548  issubcat  25213  heiborlem3  25905  rrnval  25919  ismrer1  25930  mzpincl  26180  pellexlem3  26284  pellexlem4  26285  pellexlem5  26286  aomclem6  26524  lcvfbr  28460  cmtfvalN  28650  cvrfval  28708  dvhvbase  30527  dvhfvadd  30531  dvhfvsca  30540  dibval  30582  dibfna  30594  dicval  30616  hdmap1fval  31237
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 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-rex 2524  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-opab 4052  df-xp 4675
  Copyright terms: Public domain W3C validator