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

Theorem xpex 6503
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 6502 . 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 1756   _Vcvv 2967    X. cxp 4833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-rex 2716  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-opab 4346  df-xp 4841
This theorem is referenced by:  oprabex  6560  oprabex3  6561  fnpm  7214  mapsnf1o2  7252  ixpsnf1o  7295  xpsnen  7387  endisj  7390  xpcomen  7394  xpassen  7397  xpmapenlem  7470  mapunen  7472  unxpdomlem3  7511  hartogslem1  7748  rankxpl  8074  rankfu  8076  rankmapu  8077  rankxplim  8078  rankxplim2  8079  rankxplim3  8080  rankxpsuc  8081  r0weon  8171  infxpenlem  8172  infxpenc2lem2  8178  infxpenc2lem2OLD  8182  dfac3  8283  dfac5lem2  8286  dfac5lem3  8287  dfac5lem4  8288  cdafn  8330  unctb  8366  axcc2lem  8597  axdc3lem  8611  axdc4lem  8616  enqex  9083  nqex  9084  enrex  9229  axcnex  9306  zexALT  10657  cnexALT  10979  addex  10981  mulex  10982  ixxex  11303  shftfval  12551  climconst2  13018  xpnnenOLD  13484  cpnnen  13503  ruclem13  13516  cnso  13521  prdsval  14385  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  prdsle  14392  prdsds  14394  prdshom  14397  prdsco  14398  fnmrc  14537  mrcfval  14538  mreacs  14588  comfffval  14629  oppccofval  14647  sectfval  14682  brssc  14719  sscpwex  14720  isssc  14725  isfunc  14766  isfuncd  14767  idfu2nd  14779  idfu1st  14781  idfucl  14783  wunfunc  14801  fuccofval  14861  homafval  14889  homaf  14890  homaval  14891  coapm  14931  catccofval  14960  catcfuccl  14969  xpcval  14979  xpcbas  14980  xpchom  14982  xpccofval  14984  1stfval  14993  2ndfval  14996  1stfcl  14999  2ndfcl  15000  catcxpccl  15009  evlf2  15020  evlf1  15022  evlfcl  15024  hof1fval  15055  hof2fval  15057  hofcl  15061  ipoval  15316  letsr  15389  plusffval  15419  frmdplusg  15523  eqgfval  15720  efglem  16204  efgval  16205  scaffval  16944  psrplusg  17429  ltbval  17528  opsrle  17532  evlslem2  17572  evlssca  17583  mpfind  17597  evls1sca  17733  pf1ind  17764  cnfldds  17803  xrsadd  17808  xrsmul  17809  xrsle  17811  xrsds  17831  znle  17942  ipffval  18052  pjfval  18106  2ndcctbss  19034  txuni2  19113  txbas  19115  eltx  19116  txcnp  19168  txcnmpt  19172  txrest  19179  txlm  19196  tx1stc  19198  tx2ndc  19199  txkgen  19200  txflf  19554  cnextfval  19609  distgp  19645  indistgp  19646  ustfn  19751  ustn0  19770  ussid  19810  ressuss  19813  ishtpy  20519  isphtpc  20541  elovolm  20933  elovolmr  20934  ovolmge0  20935  ovolgelb  20938  ovolunlem1a  20954  ovolunlem1  20955  ovoliunlem1  20960  ovoliunlem2  20961  ovolshftlem2  20968  ovolicc2  20980  ioombl1  21018  dyadmbl  21055  vitali  21068  mbfimaopnlem  21108  dvfval  21347  plyeq0lem  21653  taylfval  21799  ulmval  21820  dmarea  22326  dchrplusg  22561  iscgrg  22940  axlowdimlem15  23153  axlowdim  23158  iseupa  23537  isgrpoi  23636  vcoprne  23908  sspval  24072  0ofval  24138  ajfval  24160  hvmulex  24364  inftmrel  26148  isinftm  26149  tpr2rico  26294  faeval  26614  mbfmco2  26632  br2base  26636  sxbrsigalem0  26638  sxbrsigalem3  26639  dya2iocrfn  26646  dya2iocct  26647  dya2iocnrect  26648  dya2iocuni  26650  dya2iocucvr  26651  sxbrsigalem2  26653  eulerpartlemgs2  26715  ccatmulgnn0dir  26892  afsval  26947  cvmlift2lem9  27152  brimg  27919  brrestrict  27931  colinearex  28042  mblfinlem1  28381  heiborlem3  28665  rrnval  28679  ismrer1  28690  mzpincl  29023  pellexlem3  29125  pellexlem4  29126  pellexlem5  29127  aomclem6  29365  numclwwlk1  30644  mat1dimmul  30795  lcvfbr  32505  cmtfvalN  32695  cvrfval  32753  dvhvbase  34572  dvhfvadd  34576  dvhfvsca  34585  dibval  34627  dibfna  34639  dicval  34661  hdmap1fval  35282
  Copyright terms: Public domain W3C validator