Theorem xpex 7700

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   × cxp 5622

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 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-opab 5149  df-xp 5630  df-rel 5631

This theorem is referenced by:  oprabex  7922  oprabex3  7923  mpoexw  8024  naddcllem  8605  fnpm  8774  mapsnf1o2  8835  ixpsnf1o  8879  xpsnen  8992  endisj  8995  xpcomen  8999  xpassen  9002  xpmapenlem  9075  unxpdomlem3  9161  hartogslem1  9450  rankxpl  9790  rankfu  9792  rankmapu  9793  rankxplim  9794  rankxplim2  9795  rankxplim3  9796  rankxpsuc  9797  r0weon  9925  infxpenlem  9926  infxpenc2lem2  9933  dfac3  10034  dfac5lem2  10037  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  unctb  10117  axcc2lem  10349  axdc3lem  10363  axdc4lem  10368  enqex  10836  nqex  10837  nrex1  10978  enrex  10981  axcnex  11061  zexALT  12535  cnexALT  12927  mpoaddex  12929  addex  12930  mpomulex  12931  mulex  12932  ixxex  13300  shftfval  15023  climconst2  15501  cpnnen  16187  ruclem13  16200  cnso  16205  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdsle  17416  prdshom  17421  prdsco  17422  xrsle  17559  fnmrc  17564  mrcfval  17565  mreacs  17615  comfffval  17655  oppccofval  17673  sectfval  17709  brssc  17772  sscpwex  17773  isssc  17778  isfunc  17822  isfuncd  17823  idfu2nd  17835  idfu1st  17837  idfucl  17839  wunfunc  17859  fuccofval  17920  homafval  17987  homaf  17988  homaval  17989  coapm  18029  catccofval  18062  catcfuccl  18076  xpcval  18134  xpcbas  18135  xpchom  18137  xpccofval  18139  1stfval  18148  2ndfval  18151  1stfcl  18154  2ndfcl  18155  catcxpccl  18164  evlf2  18175  evlf1  18177  evlfcl  18179  hof1fval  18210  hof2fval  18212  hofcl  18216  ipoval  18487  letsr  18550  frmdplusg  18813  smndex1gbas  18861  smndex1gid  18863  smndex1igid  18865  eqgfval  19142  efglem  19682  efgval  19683  cnfldds  21356  cnfldfun  21358  cnfldfunALT  21359  cnflddsOLD  21369  cnfldfunOLD  21371  cnfldfunALTOLD  21372  xrsadd  21375  xrsmul  21376  xrsds  21399  pzriprnglem13  21483  pzriprnglem14  21484  znle  21526  pjfval  21696  psrplusg  21926  ltbval  22031  opsrle  22035  evlslem2  22067  evlsvvval  22081  evlssca  22082  mpfind  22103  psdmul  22142  evls1sca  22298  pf1ind  22330  mat1dimmul  22451  2ndcctbss  23430  txuni2  23540  txbas  23542  eltx  23543  txcnp  23595  txcnmpt  23599  txrest  23606  txlm  23623  tx1stc  23625  tx2ndc  23626  txkgen  23627  txflf  23981  cnextfval  24037  distgp  24074  indistgp  24075  ustfn  24177  ustn0  24196  ussid  24235  ressuss  24237  ishtpy  24949  isphtpc  24971  elovolmlem  25451  dyadmbl  25577  vitali  25590  mbfimaopnlem  25632  dvfval  25874  plyeq0lem  26185  taylfval  26335  ulmval  26358  dmarea  26934  dchrplusg  27224  madefi  27919  addsval  27968  mulsval  28115  zsex  28386  istrkg2ld  28542  tgjustc1  28557  tgjustc2  28558  iscgrg  28594  ishlg  28684  ishpg  28841  iscgra  28891  isinag  28920  isleag  28929  axlowdimlem15  29039  axlowdim  29044  isgrpoi  30584  sspval  30809  0ofval  30873  ajfval  30895  hvmulex  31097  padct  32806  gsumwrd2dccat  33154  inftmrel  33256  isinftm  33257  smatrcl  33956  tpr2rico  34072  faeval  34406  mbfmco2  34425  br2base  34429  sxbrsigalem0  34431  sxbrsigalem3  34432  dya2iocrfn  34439  dya2iocct  34440  dya2iocnrect  34441  dya2iocuni  34443  dya2iocucvr  34444  sxbrsigalem2  34446  eulerpartlemgs2  34540  ccatmulgnn0dir  34702  afsval  34831  cvmlift2lem9  35509  satfv0  35556  satf00  35572  prv1n  35629  mexval  35700  mdvval  35702  mpstval  35733  brimg  36133  brrestrict  36147  colinearex  36258  poimirlem4  37959  poimirlem28  37983  mblfinlem1  37992  heiborlem3  38148  rrnval  38162  ismrer1  38173  dfcnvrefrels2  38943  dfcnvrefrels3  38944  lcvfbr  39480  cmtfvalN  39670  cvrfval  39728  dvhvbase  41547  dvhfvadd  41551  dvhfvsca  41560  dibval  41602  dibfna  41614  dicval  41636  hdmap1fval  42256  ltex  42698  leex  42699  subex  42700  mzpincl  43180  pellexlem3  43277  pellexlem4  43278  pellexlem5  43279  aomclem6  43505  trclexi  44065  rtrclexi  44066  brtrclfv2  44172  mnringmulrcld  44673  hoiprodcl2  47001  hoicvrrex  47002  ovn0lem  47011  ovnhoilem1  47047  ovnlecvr2  47056  opnvonmbllem1  47078  opnvonmbllem2  47079  ovolval2lem  47089  ovolval2  47090  ovolval3  47093  ovolval4lem2  47096  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  smflimlem6  47222  gpgvtx  48531  gpgiedg  48532  sectfn  49516  nelsubc3  49558  cofidvala  49603  cofidval  49606  diag1f1lem  49793  fucoelvv  49807  fucofvalne  49812  functhinclem1  49931  functhinclem3  49933  functermc2  49996  idfudiag1bas  50011  idfudiag1  50012  prstchomval  50046  elpglem3  50200  pgindnf  50203  aacllem  50288