Theorem xpex 7732

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 7729	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
4	1, 2, 3	mp2an 702	1 ⊢ (𝐴 × 𝐵) ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 3453   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-opab 5162  df-xp 5651  df-rel 5652

This theorem is referenced by:  oprabex  7953  oprabex3  7954  mpoexw  8055  naddcllem  8641  fnpm  8811  mapsnf1o2  8872  ixpsnf1o  8916  xpsnen  9029  endisj  9032  xpcomen  9036  xpassen  9039  xpmapenlem  9112  unxpdomlem3  9198  hartogslem1  9487  rankxpl  9830  rankfu  9832  rankmapu  9833  rankxplim  9834  rankxplim2  9835  rankxplim3  9836  rankxpsuc  9837  r0weon  9965  infxpenlem  9966  infxpenc2lem2  9973  dfac3  10074  dfac5lem2  10077  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  unctb  10157  axcc2lem  10390  axdc3lem  10404  axdc4lem  10409  enqex  10877  nqex  10878  nrex1  11019  enrex  11022  axcnex  11102  zexALT  12585  cnexALT  12984  mpoaddex  12986  addex  12987  mpomulex  12988  mulex  12989  ixxex  13357  shftfval  15080  climconst2  15558  cpnnen  16244  ruclem13  16257  cnso  16262  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdsle  17474  prdshom  17479  prdsco  17480  xrsle  17617  fnmrc  17622  mrcfval  17623  mreacs  17673  comfffval  17713  oppccofval  17731  sectfval  17767  brssc  17830  sscpwex  17831  isssc  17836  isfunc  17880  isfuncd  17881  idfu2nd  17893  idfu1st  17895  idfucl  17897  wunfunc  17917  fuccofval  17978  homafval  18045  homaf  18046  homaval  18047  coapm  18087  catccofval  18120  catcfuccl  18134  xpcval  18192  xpcbas  18193  xpchom  18195  xpccofval  18197  1stfval  18206  2ndfval  18209  1stfcl  18212  2ndfcl  18213  catcxpccl  18222  evlf2  18233  evlf1  18235  evlfcl  18237  hof1fval  18268  hof2fval  18270  hofcl  18274  ipoval  18545  letsr  18608  frmdplusg  18871  smndex1gbas  18919  smndex1gid  18921  smndex1igid  18923  eqgfval  19200  efglem  19739  efgval  19740  cnfldds  21416  cnfldfun  21418  cnfldfunALT  21419  xrsadd  21422  xrsmul  21423  xrsds  21442  pzriprnglem13  21525  pzriprnglem14  21526  znle  21568  pjfval  21738  psrplusg  21969  ltbval  22076  opsrle  22080  evlslem2  22112  evlsvvval  22126  evlssca  22127  mpfind  22148  psdmul  22211  evls1sca  22366  pf1ind  22398  mat1dimmul  22516  2ndcctbss  23495  txuni2  23605  txbas  23607  eltx  23608  txcnp  23660  txcnmpt  23664  txrest  23671  txlm  23688  tx1stc  23690  tx2ndc  23691  txkgen  23692  txflf  24046  cnextfval  24102  distgp  24139  indistgp  24140  ustfn  24242  ustn0  24261  ussid  24300  ressuss  24302  ishtpy  25014  isphtpc  25036  elovolmlem  25516  dyadmbl  25642  vitali  25655  mbfimaopnlem  25697  dvfval  25939  plyeq0lem  26250  taylfval  26399  ulmval  26420  dmarea  26999  dchrplusg  27288  madefi  27983  addsval  28032  mulsval  28179  zsex  28450  istrkg2ld  28606  tgjustc1  28621  tgjustc2  28622  iscgrg  28658  ishlg  28748  ishpg  28905  iscgra  28955  isinag  28984  isleag  28993  axlowdimlem15  29103  axlowdim  29108  isgrpoi  30647  sspval  30872  0ofval  30936  ajfval  30958  hvmulex  31160  padct  32870  gsumwrd2dccat  33219  inftmrel  33321  isinftm  33322  smatrcl  34054  tpr2rico  34170  faeval  34504  mbfmco2  34523  br2base  34527  sxbrsigalem0  34529  sxbrsigalem3  34530  dya2iocrfn  34537  dya2iocct  34538  dya2iocnrect  34539  dya2iocuni  34541  dya2iocucvr  34542  sxbrsigalem2  34544  eulerpartlemgs2  34638  ccatmulgnn0dir  34800  afsval  34932  cvmlift2lem9  35625  satfv0  35672  satf00  35688  prv1n  35745  mexval  35816  mdvval  35818  mpstval  35849  brimg  36249  brrestrict  36263  colinearex  36374  nmulprop  36504  poimirlem4  38087  poimirlem28  38111  mblfinlem1  38120  heiborlem3  38276  rrnval  38290  ismrer1  38301  dfcnvrefrels2  39071  dfcnvrefrels3  39072  lcvfbr  39608  cmtfvalN  39798  cvrfval  39856  dvhvbase  41675  dvhfvadd  41679  dvhfvsca  41688  dibval  41730  dibfna  41742  dicval  41764  hdmap1fval  42384  ltex  42825  leex  42826  subex  42827  mzpincl  43279  pellexlem3  43372  pellexlem4  43373  pellexlem5  43374  aomclem6  43600  trclexi  44160  rtrclexi  44161  brtrclfv2  44267  mnringmulrcld  44768  hoiprodcl2  47093  hoicvrrex  47094  ovn0lem  47103  ovnhoilem1  47139  ovnlecvr2  47148  opnvonmbllem1  47170  opnvonmbllem2  47171  ovolval2lem  47181  ovolval2  47182  ovolval3  47185  ovolval4lem2  47188  ovolval5lem2  47191  ovnovollem1  47194  ovnovollem2  47195  smflimlem6  47314  gpgvtx  48629  gpgiedg  48630  sectfn  49614  nelsubc3  49656  cofidvala  49701  cofidval  49704  diag1f1lem  49891  fucoelvv  49905  fucofvalne  49910  functhinclem1  50029  functhinclem3  50031  functermc2  50094  idfudiag1bas  50109  idfudiag1  50110  prstchomval  50144  elpglem3  50298  pgindnf  50301  aacllem  50386