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

Theorem xpex 4754
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 4753 . 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 2740    X. cxp 4624
This theorem is referenced by:  oprabex  5860  oprabex3  5861  fnpm  6713  mapsnf1o2  6748  ixpsnf1o  6789  xpsnen  6879  endisj  6882  xpcomen  6886  xpassen  6889  xpmapenlem  6961  mapunen  6963  unxpdomlem3  7002  hartogslem1  7190  rankxpl  7480  rankxplim  7482  rankxplim2  7483  rankxplim3  7484  rankxpsuc  7485  r0weon  7573  infxpenlem  7574  infxpenc2lem2  7580  dfac3  7681  dfac5lem2  7684  dfac5lem3  7685  dfac5lem4  7686  cdafn  7728  unctb  7764  axcc2lem  7995  axdc3lem  8009  axdc4lem  8014  enqex  8479  nqex  8480  enrex  8625  axcnex  8702  zexALT  9974  cnexALT  10282  addex  10284  mulex  10285  ixxex  10598  shftfval  11495  climconst2  11952  xpnnenOLD  12415  cpnnen  12434  ruclem13  12447  cnso  12452  prdsval  13282  prdsplusg  13285  prdsmulr  13286  prdsvsca  13287  prdsle  13288  prdsds  13290  prdshom  13293  prdsco  13294  fnmrc  13436  mrcfval  13437  mreacs  13487  comfffval  13528  oppccofval  13546  sectfval  13581  brssc  13618  sscpwex  13619  isssc  13624  isfunc  13665  isfuncd  13666  idfu2nd  13678  idfu1st  13680  idfucl  13682  wunfunc  13700  fuccofval  13760  homafval  13788  homaf  13789  homaval  13790  coapm  13830  catccofval  13859  catcfuccl  13868  fnxpc  13877  xpcval  13878  xpcbas  13879  xpchom  13881  xpccofval  13883  1stfval  13892  2ndfval  13895  1stfcl  13898  2ndfcl  13899  catcxpccl  13908  evlf2  13919  evlf1  13921  evlfcl  13923  hof1fval  13954  hof2fval  13956  hofcl  13960  ipoval  14184  letsr  14276  plusffval  14306  frmdplusg  14403  eqgfval  14592  efglem  14952  efgval  14953  scaffval  15572  psrplusg  16053  ltbval  16140  opsrle  16144  evlslem2  16176  cnfldds  16316  xrsadd  16318  xrsmul  16319  xrsle  16321  xrsds  16341  znle  16417  ipffval  16479  pjfval  16533  2ndcctbss  17108  txuni2  17187  txbas  17189  eltx  17190  txcnp  17241  txcnmpt  17245  txrest  17252  txlm  17269  tx1stc  17271  tx2ndc  17272  txkgen  17273  txflf  17628  distgp  17709  indistgp  17710  ishtpy  18397  isphtpc  18419  elovolm  18761  elovolmr  18762  ovolmge0  18763  ovolgelb  18766  ovolunlem1a  18782  ovolunlem1  18783  ovoliunlem1  18788  ovoliunlem2  18789  ovolshftlem2  18796  ovolicc2  18808  ioombl1  18846  dyadmbl  18882  vitali  18895  mbfimaopnlem  18937  dvfval  19174  evlssca  19333  mpfind  19355  pf1ind  19365  plyeq0lem  19519  taylfval  19665  ulmval  19686  dmarea  20179  dchrplusg  20413  isgrpoi  20790  vcoprne  21060  sspval  21224  0ofval  21290  ajfval  21312  hvmulex  21516  cvmlift2lem9  23179  iseupa  23218  brimg  23816  brrestrict  23827  axlowdimlem15  23924  axlowdim  23929  colinearex  24023  nZdef  24512  issubcat  25177  heiborlem3  25869  rrnval  25883  ismrer1  25894  mzpincl  26144  pellexlem3  26248  pellexlem4  26249  pellexlem5  26250  aomclem6  26488  lcvfbr  28340  cmtfvalN  28530  cvrfval  28588  dvhvbase  30407  dvhfvadd  30411  dvhfvsca  30420  dibval  30462  dibfna  30474  dicval  30496  hdmap1fval  31117
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 2237  ax-sep 4081  ax-nul 4089  ax-pow 4126  ax-pr 4152  ax-un 4449
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rex 2521  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-opab 4018  df-xp 4640
  Copyright terms: Public domain W3C validator