Theorem xpex 7707

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	⊢ 𝐴 ∈ V
xpex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
xpex	⊢ (𝐴 × 𝐵) ∈ V

Proof of Theorem xpex

Step	Hyp	Ref	Expression
1		xpex.1	. 2 ⊢ 𝐴 ∈ V
2		xpex.2	. 2 ⊢ 𝐵 ∈ V
3		xpexg 7704	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴 × 𝐵) ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  oprabex  7929  oprabex3  7930  mpoexw  8031  naddcllem  8612  fnpm  8781  mapsnf1o2  8842  ixpsnf1o  8886  xpsnen  8999  endisj  9002  xpcomen  9006  xpassen  9009  xpmapenlem  9082  unxpdomlem3  9168  hartogslem1  9457  rankxpl  9799  rankfu  9801  rankmapu  9802  rankxplim  9803  rankxplim2  9804  rankxplim3  9805  rankxpsuc  9806  r0weon  9934  infxpenlem  9935  infxpenc2lem2  9942  dfac3  10043  dfac5lem2  10046  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  unctb  10126  axcc2lem  10358  axdc3lem  10372  axdc4lem  10377  enqex  10845  nqex  10846  nrex1  10987  enrex  10990  axcnex  11070  zexALT  12544  cnexALT  12936  mpoaddex  12938  addex  12939  mpomulex  12940  mulex  12941  ixxex  13309  shftfval  15032  climconst2  15510  cpnnen  16196  ruclem13  16209  cnso  16214  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdsle  17425  prdshom  17430  prdsco  17431  xrsle  17568  fnmrc  17573  mrcfval  17574  mreacs  17624  comfffval  17664  oppccofval  17682  sectfval  17718  brssc  17781  sscpwex  17782  isssc  17787  isfunc  17831  isfuncd  17832  idfu2nd  17844  idfu1st  17846  idfucl  17848  wunfunc  17868  fuccofval  17929  homafval  17996  homaf  17997  homaval  17998  coapm  18038  catccofval  18071  catcfuccl  18085  xpcval  18143  xpcbas  18144  xpchom  18146  xpccofval  18148  1stfval  18157  2ndfval  18160  1stfcl  18163  2ndfcl  18164  catcxpccl  18173  evlf2  18184  evlf1  18186  evlfcl  18188  hof1fval  18219  hof2fval  18221  hofcl  18225  ipoval  18496  letsr  18559  frmdplusg  18822  smndex1gbas  18870  smndex1gid  18872  smndex1igid  18874  eqgfval  19151  efglem  19691  efgval  19692  cnfldds  21364  cnfldfun  21366  cnfldfunALT  21367  xrsadd  21370  xrsmul  21371  xrsds  21390  pzriprnglem13  21473  pzriprnglem14  21474  znle  21516  pjfval  21686  psrplusg  21916  ltbval  22021  opsrle  22025  evlslem2  22057  evlsvvval  22071  evlssca  22072  mpfind  22093  psdmul  22132  evls1sca  22288  pf1ind  22320  mat1dimmul  22441  2ndcctbss  23420  txuni2  23530  txbas  23532  eltx  23533  txcnp  23585  txcnmpt  23589  txrest  23596  txlm  23613  tx1stc  23615  tx2ndc  23616  txkgen  23617  txflf  23971  cnextfval  24027  distgp  24064  indistgp  24065  ustfn  24167  ustn0  24186  ussid  24225  ressuss  24227  ishtpy  24939  isphtpc  24961  elovolmlem  25441  dyadmbl  25567  vitali  25580  mbfimaopnlem  25622  dvfval  25864  plyeq0lem  26175  taylfval  26324  ulmval  26345  dmarea  26921  dchrplusg  27210  madefi  27905  addsval  27954  mulsval  28101  zsex  28372  istrkg2ld  28528  tgjustc1  28543  tgjustc2  28544  iscgrg  28580  ishlg  28670  ishpg  28827  iscgra  28877  isinag  28906  isleag  28915  axlowdimlem15  29025  axlowdim  29030  isgrpoi  30569  sspval  30794  0ofval  30858  ajfval  30880  hvmulex  31082  padct  32791  gsumwrd2dccat  33139  inftmrel  33241  isinftm  33242  smatrcl  33940  tpr2rico  34056  faeval  34390  mbfmco2  34409  br2base  34413  sxbrsigalem0  34415  sxbrsigalem3  34416  dya2iocrfn  34423  dya2iocct  34424  dya2iocnrect  34425  dya2iocuni  34427  dya2iocucvr  34428  sxbrsigalem2  34430  eulerpartlemgs2  34524  ccatmulgnn0dir  34686  afsval  34815  cvmlift2lem9  35493  satfv0  35540  satf00  35556  prv1n  35613  mexval  35684  mdvval  35686  mpstval  35717  brimg  36117  brrestrict  36131  colinearex  36242  poimirlem4  37945  poimirlem28  37969  mblfinlem1  37978  heiborlem3  38134  rrnval  38148  ismrer1  38159  dfcnvrefrels2  38929  dfcnvrefrels3  38930  lcvfbr  39466  cmtfvalN  39656  cvrfval  39714  dvhvbase  41533  dvhfvadd  41537  dvhfvsca  41546  dibval  41588  dibfna  41600  dicval  41622  hdmap1fval  42242  ltex  42684  leex  42685  subex  42686  mzpincl  43166  pellexlem3  43259  pellexlem4  43260  pellexlem5  43261  aomclem6  43487  trclexi  44047  rtrclexi  44048  brtrclfv2  44154  mnringmulrcld  44655  hoiprodcl2  46983  hoicvrrex  46984  ovn0lem  46993  ovnhoilem1  47029  ovnlecvr2  47038  opnvonmbllem1  47060  opnvonmbllem2  47061  ovolval2lem  47071  ovolval2  47072  ovolval3  47075  ovolval4lem2  47078  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  smflimlem6  47204  gpgvtx  48519  gpgiedg  48520  sectfn  49504  nelsubc3  49546  cofidvala  49591  cofidval  49594  diag1f1lem  49781  fucoelvv  49795  fucofvalne  49800  functhinclem1  49919  functhinclem3  49921  functermc2  49984  idfudiag1bas  49999  idfudiag1  50000  prstchomval  50034  elpglem3  50188  pgindnf  50191  aacllem  50276