Theorem xpex 7737

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-opab 5211  df-xp 5682  df-rel 5683

This theorem is referenced by:  oprabex  7960  oprabex3  7961  mpoexw  8062  naddcllem  8672  fnpm  8825  mapsnf1o2  8885  ixpsnf1o  8929  xpsnen  9052  endisj  9055  xpcomen  9060  xpassen  9063  xpmapenlem  9141  unxpdomlem3  9249  hartogslem1  9534  rankxpl  9867  rankfu  9869  rankmapu  9870  rankxplim  9871  rankxplim2  9872  rankxplim3  9873  rankxpsuc  9874  r0weon  10004  infxpenlem  10005  infxpenc2lem2  10012  dfac3  10113  dfac5lem2  10116  dfac5lem3  10117  dfac5lem4  10118  unctb  10197  axcc2lem  10428  axdc3lem  10442  axdc4lem  10447  enqex  10914  nqex  10915  nrex1  11056  enrex  11059  axcnex  11139  zexALT  12575  cnexALT  12967  addex  12969  mulex  12970  ixxex  13332  shftfval  15014  climconst2  15489  cpnnen  16169  ruclem13  16182  cnso  16187  prdsplusg  17401  prdsmulr  17402  prdsvsca  17403  prdsle  17405  prdshom  17410  prdsco  17411  fnmrc  17548  mrcfval  17549  mreacs  17599  comfffval  17639  oppccofval  17658  sectfval  17695  brssc  17758  sscpwex  17759  isssc  17764  isfunc  17811  isfuncd  17812  idfu2nd  17824  idfu1st  17826  idfucl  17828  wunfunc  17846  wunfuncOLD  17847  fuccofval  17908  homafval  17976  homaf  17977  homaval  17978  coapm  18018  catccofval  18051  catcfuccl  18066  catcfucclOLD  18067  xpcval  18126  xpcbas  18127  xpchom  18129  xpccofval  18131  1stfval  18140  2ndfval  18143  1stfcl  18146  2ndfcl  18147  catcxpccl  18156  catcxpcclOLD  18157  evlf2  18168  evlf1  18170  evlfcl  18172  hof1fval  18203  hof2fval  18205  hofcl  18209  ipoval  18480  letsr  18543  frmdplusg  18732  eqgfval  19051  efglem  19579  efgval  19580  cnfldds  20947  cnfldfun  20949  cnfldfunALT  20950  cnfldfunALTOLD  20951  xrsadd  20955  xrsmul  20956  xrsle  20958  xrsds  20981  znle  21080  pjfval  21253  psrplusg  21492  ltbval  21590  opsrle  21594  evlslem2  21634  evlssca  21644  mpfind  21662  evls1sca  21834  pf1ind  21866  mat1dimmul  21970  2ndcctbss  22951  txuni2  23061  txbas  23063  eltx  23064  txcnp  23116  txcnmpt  23120  txrest  23127  txlm  23144  tx1stc  23146  tx2ndc  23147  txkgen  23148  txflf  23502  cnextfval  23558  distgp  23595  indistgp  23596  ustfn  23698  ustn0  23717  ussid  23757  ressuss  23759  ishtpy  24480  isphtpc  24502  elovolmlem  24983  dyadmbl  25109  vitali  25122  mbfimaopnlem  25164  dvfval  25406  plyeq0lem  25716  taylfval  25863  ulmval  25884  dmarea  26452  dchrplusg  26740  addsval  27436  mulsval  27555  tgjustc1  27716  tgjustc2  27717  iscgrg  27753  ishlg  27843  ishpg  28000  iscgra  28050  isinag  28079  isleag  28088  axlowdimlem15  28204  axlowdim  28209  isgrpoi  29739  sspval  29964  0ofval  30028  ajfval  30050  hvmulex  30252  inftmrel  32314  isinftm  32315  smatrcl  32765  tpr2rico  32881  faeval  33233  mbfmco2  33253  br2base  33257  sxbrsigalem0  33259  sxbrsigalem3  33260  dya2iocrfn  33267  dya2iocct  33268  dya2iocnrect  33269  dya2iocuni  33271  dya2iocucvr  33272  sxbrsigalem2  33274  eulerpartlemgs2  33368  ccatmulgnn0dir  33542  afsval  33672  cvmlift2lem9  34291  satfv0  34338  satf00  34354  prv1n  34411  mexval  34482  mdvval  34484  mpstval  34515  brimg  34898  brrestrict  34910  colinearex  35021  poimirlem4  36481  poimirlem28  36505  mblfinlem1  36514  heiborlem3  36670  rrnval  36684  ismrer1  36695  dfcnvrefrels2  37387  dfcnvrefrels3  37388  lcvfbr  37879  cmtfvalN  38069  cvrfval  38127  dvhvbase  39947  dvhfvadd  39951  dvhfvsca  39960  dibval  40002  dibfna  40014  dicval  40036  hdmap1fval  40656  evlsvvval  41133  mzpincl  41458  pellexlem3  41555  pellexlem4  41556  pellexlem5  41557  aomclem6  41787  trclexi  42357  rtrclexi  42358  brtrclfv2  42464  mnringmulrcld  42973  hoiprodcl2  45258  hoicvrrex  45259  ovn0lem  45268  ovnhoilem1  45304  ovnlecvr2  45313  opnvonmbllem1  45335  opnvonmbllem2  45336  ovolval2lem  45346  ovolval2  45347  ovolval3  45350  ovolval4lem2  45353  ovolval5lem2  45356  ovnovollem1  45359  ovnovollem2  45360  smflimlem6  45479  functhinclem1  47615  functhinclem3  47617  prstchomval  47648  elpglem3  47712  pgindnf  47715  aacllem  47802