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

Theorem xpex 4949
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 4948 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 654 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916    X. cxp 4835
This theorem is referenced by:  oprabex  6146  oprabex3  6147  fnpm  6985  mapsnf1o2  7020  ixpsnf1o  7061  xpsnen  7151  endisj  7154  xpcomen  7158  xpassen  7161  xpmapenlem  7233  mapunen  7235  unxpdomlem3  7274  hartogslem1  7467  rankxpl  7757  rankxplim  7759  rankxplim2  7760  rankxplim3  7761  rankxpsuc  7762  r0weon  7850  infxpenlem  7851  infxpenc2lem2  7857  dfac3  7958  dfac5lem2  7961  dfac5lem3  7962  dfac5lem4  7963  cdafn  8005  unctb  8041  axcc2lem  8272  axdc3lem  8286  axdc4lem  8291  enqex  8755  nqex  8756  enrex  8901  axcnex  8978  zexALT  10256  cnexALT  10564  addex  10566  mulex  10567  ixxex  10883  shftfval  11840  climconst2  12297  xpnnenOLD  12764  cpnnen  12783  ruclem13  12796  cnso  12801  prdsval  13633  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdsle  13639  prdsds  13641  prdshom  13644  prdsco  13645  fnmrc  13787  mrcfval  13788  mreacs  13838  comfffval  13879  oppccofval  13897  sectfval  13932  brssc  13969  sscpwex  13970  isssc  13975  isfunc  14016  isfuncd  14017  idfu2nd  14029  idfu1st  14031  idfucl  14033  wunfunc  14051  fuccofval  14111  homafval  14139  homaf  14140  homaval  14141  coapm  14181  catccofval  14210  catcfuccl  14219  fnxpc  14228  xpcval  14229  xpcbas  14230  xpchom  14232  xpccofval  14234  1stfval  14243  2ndfval  14246  1stfcl  14249  2ndfcl  14250  catcxpccl  14259  evlf2  14270  evlf1  14272  evlfcl  14274  hof1fval  14305  hof2fval  14307  hofcl  14311  ipoval  14535  letsr  14627  plusffval  14657  frmdplusg  14754  eqgfval  14943  efglem  15303  efgval  15304  scaffval  15923  psrplusg  16400  ltbval  16487  opsrle  16491  evlslem2  16523  cnfldds  16668  xrsadd  16673  xrsmul  16674  xrsle  16676  xrsds  16696  znle  16772  ipffval  16834  pjfval  16888  2ndcctbss  17471  txuni2  17550  txbas  17552  eltx  17553  txcnp  17605  txcnmpt  17609  txrest  17616  txlm  17633  tx1stc  17635  tx2ndc  17636  txkgen  17637  txflf  17991  cnextfval  18046  distgp  18082  indistgp  18083  ustfn  18184  ustn0  18203  ussid  18243  ressuss  18246  ishtpy  18950  isphtpc  18972  elovolm  19324  elovolmr  19325  ovolmge0  19326  ovolgelb  19329  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovolshftlem2  19359  ovolicc2  19371  ioombl1  19409  dyadmbl  19445  vitali  19458  mbfimaopnlem  19500  dvfval  19737  evlssca  19896  mpfind  19918  pf1ind  19928  plyeq0lem  20082  taylfval  20228  ulmval  20249  dmarea  20749  dchrplusg  20984  iseupa  21640  isgrpoi  21739  vcoprne  22011  sspval  22175  0ofval  22241  ajfval  22263  hvmulex  22467  inftmrel  24203  isinftm  24204  tpr2rico  24263  faeval  24550  mbfmco2  24568  br2base  24572  sxbrsigalem0  24574  sxbrsigalem3  24575  dya2iocrfn  24582  dya2iocct  24583  dya2iocnrect  24584  dya2iocuni  24586  dya2iocucvr  24587  sxbrsigalem2  24589  cvmlift2lem9  24951  brimg  25690  brrestrict  25702  axlowdimlem15  25799  axlowdim  25804  colinearex  25898  mblfinlem  26143  heiborlem3  26412  rrnval  26426  ismrer1  26437  mzpincl  26681  pellexlem3  26784  pellexlem4  26785  pellexlem5  26786  aomclem6  27024  lcvfbr  29503  cmtfvalN  29693  cvrfval  29751  dvhvbase  31570  dvhfvadd  31574  dvhfvsca  31583  dibval  31625  dibfna  31637  dicval  31659  hdmap1fval  32280
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-opab 4227  df-xp 4843
  Copyright terms: Public domain W3C validator