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

Theorem xpex 6712
Description: The Cartesian 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 6710 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  X.  B
)  e.  _V )
41, 2, 3mp2an 672 1  |-  ( A  X.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113    X. cxp 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rex 2820  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-opab 4506  df-xp 5005
This theorem is referenced by:  oprabex  6772  oprabex3  6773  fnpm  7428  mapsnf1o2  7466  ixpsnf1o  7509  xpsnen  7601  endisj  7604  xpcomen  7608  xpassen  7611  xpmapenlem  7684  mapunen  7686  unxpdomlem3  7726  hartogslem1  7966  rankxpl  8292  rankfu  8294  rankmapu  8295  rankxplim  8296  rankxplim2  8297  rankxplim3  8298  rankxpsuc  8299  r0weon  8389  infxpenlem  8390  infxpenc2lem2  8396  infxpenc2lem2OLD  8400  dfac3  8501  dfac5lem2  8504  dfac5lem3  8505  dfac5lem4  8506  cdafn  8548  unctb  8584  axcc2lem  8815  axdc3lem  8829  axdc4lem  8834  enqex  9299  nqex  9300  enrex  9443  axcnex  9523  zexALT  10882  cnexALT  11215  addex  11217  mulex  11218  ixxex  11539  shftfval  12865  climconst2  13333  xpnnenOLD  13803  cpnnen  13822  ruclem13  13835  cnso  13840  prdsval  14709  prdsplusg  14712  prdsmulr  14713  prdsvsca  14714  prdsle  14716  prdsds  14718  prdshom  14721  prdsco  14722  fnmrc  14861  mrcfval  14862  mreacs  14912  comfffval  14953  oppccofval  14971  sectfval  15006  brssc  15043  sscpwex  15044  isssc  15049  isfunc  15090  isfuncd  15091  idfu2nd  15103  idfu1st  15105  idfucl  15107  wunfunc  15125  fuccofval  15185  homafval  15213  homaf  15214  homaval  15215  coapm  15255  catccofval  15284  catcfuccl  15293  xpcval  15303  xpcbas  15304  xpchom  15306  xpccofval  15308  1stfval  15317  2ndfval  15320  1stfcl  15323  2ndfcl  15324  catcxpccl  15333  evlf2  15344  evlf1  15346  evlfcl  15348  hof1fval  15379  hof2fval  15381  hofcl  15385  ipoval  15640  letsr  15713  plusffval  15743  frmdplusg  15851  eqgfval  16051  efglem  16537  efgval  16538  scaffval  17325  psrplusg  17821  ltbval  17923  opsrle  17927  evlslem2  17967  evlssca  17978  mpfind  17992  evls1sca  18147  pf1ind  18178  cnfldds  18217  xrsadd  18222  xrsmul  18223  xrsle  18225  xrsds  18245  znle  18356  ipffval  18466  pjfval  18520  mat1dimmul  18761  2ndcctbss  19738  txuni2  19817  txbas  19819  eltx  19820  txcnp  19872  txcnmpt  19876  txrest  19883  txlm  19900  tx1stc  19902  tx2ndc  19903  txkgen  19904  txflf  20258  cnextfval  20313  distgp  20349  indistgp  20350  ustfn  20455  ustn0  20474  ussid  20514  ressuss  20517  ishtpy  21223  isphtpc  21245  elovolm  21637  elovolmr  21638  ovolmge0  21639  ovolgelb  21642  ovolunlem1a  21658  ovolunlem1  21659  ovoliunlem1  21664  ovoliunlem2  21665  ovolshftlem2  21672  ovolicc2  21684  ioombl1  21723  dyadmbl  21760  vitali  21773  mbfimaopnlem  21813  dvfval  22052  plyeq0lem  22358  taylfval  22504  ulmval  22525  dmarea  23031  dchrplusg  23266  iscgrg  23648  axlowdimlem15  23951  axlowdim  23956  iseupa  24657  numclwwlk1  24791  isgrpoi  24892  vcoprne  25164  sspval  25328  0ofval  25394  ajfval  25416  hvmulex  25620  inftmrel  27402  isinftm  27403  tpr2rico  27546  faeval  27874  mbfmco2  27892  br2base  27896  sxbrsigalem0  27898  sxbrsigalem3  27899  dya2iocrfn  27906  dya2iocct  27907  dya2iocnrect  27908  dya2iocuni  27910  dya2iocucvr  27911  sxbrsigalem2  27913  eulerpartlemgs2  27975  ccatmulgnn0dir  28152  afsval  28207  cvmlift2lem9  28412  brimg  29180  brrestrict  29192  colinearex  29303  mblfinlem1  29644  heiborlem3  29928  rrnval  29942  ismrer1  29953  mzpincl  30286  pellexlem3  30387  pellexlem4  30388  pellexlem5  30389  aomclem6  30625  lcvfbr  33826  cmtfvalN  34016  cvrfval  34074  dvhvbase  35893  dvhfvadd  35897  dvhfvsca  35906  dibval  35948  dibfna  35960  dicval  35982  hdmap1fval  36603  trclub  36803  trclubg  36804
  Copyright terms: Public domain W3C validator