Theorem xpex 7729

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  oprabex  7955  oprabex3  7956  mpoexw  8057  naddcllem  8640  fnpm  8807  mapsnf1o2  8867  ixpsnf1o  8911  xpsnen  9025  endisj  9028  xpcomen  9032  xpassen  9035  xpmapenlem  9108  unxpdomlem3  9199  hartogslem1  9495  rankxpl  9828  rankfu  9830  rankmapu  9831  rankxplim  9832  rankxplim2  9833  rankxplim3  9834  rankxpsuc  9835  r0weon  9965  infxpenlem  9966  infxpenc2lem2  9973  dfac3  10074  dfac5lem2  10077  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  unctb  10157  axcc2lem  10389  axdc3lem  10403  axdc4lem  10408  enqex  10875  nqex  10876  nrex1  11017  enrex  11020  axcnex  11100  zexALT  12549  cnexALT  12945  mpoaddex  12947  addex  12948  mpomulex  12949  mulex  12950  ixxex  13317  shftfval  15036  climconst2  15514  cpnnen  16197  ruclem13  16210  cnso  16215  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdsle  17425  prdshom  17430  prdsco  17431  fnmrc  17568  mrcfval  17569  mreacs  17619  comfffval  17659  oppccofval  17677  sectfval  17713  brssc  17776  sscpwex  17777  isssc  17782  isfunc  17826  isfuncd  17827  idfu2nd  17839  idfu1st  17841  idfucl  17843  wunfunc  17863  fuccofval  17924  homafval  17991  homaf  17992  homaval  17993  coapm  18033  catccofval  18066  catcfuccl  18080  xpcval  18138  xpcbas  18139  xpchom  18141  xpccofval  18143  1stfval  18152  2ndfval  18155  1stfcl  18158  2ndfcl  18159  catcxpccl  18168  evlf2  18179  evlf1  18181  evlfcl  18183  hof1fval  18214  hof2fval  18216  hofcl  18220  ipoval  18489  letsr  18552  frmdplusg  18781  eqgfval  19108  efglem  19646  efgval  19647  cnfldds  21276  cnfldfun  21278  cnfldfunALT  21279  cnflddsOLD  21289  cnfldfunOLD  21291  cnfldfunALTOLD  21292  xrsadd  21296  xrsmul  21297  xrsle  21299  xrsds  21326  pzriprnglem13  21403  pzriprnglem14  21404  znle  21446  pjfval  21615  psrplusg  21845  ltbval  21950  opsrle  21954  evlslem2  21986  evlssca  21996  mpfind  22014  psdmul  22053  evls1sca  22210  pf1ind  22242  mat1dimmul  22363  2ndcctbss  23342  txuni2  23452  txbas  23454  eltx  23455  txcnp  23507  txcnmpt  23511  txrest  23518  txlm  23535  tx1stc  23537  tx2ndc  23538  txkgen  23539  txflf  23893  cnextfval  23949  distgp  23986  indistgp  23987  ustfn  24089  ustn0  24108  ussid  24148  ressuss  24150  ishtpy  24871  isphtpc  24893  elovolmlem  25375  dyadmbl  25501  vitali  25514  mbfimaopnlem  25556  dvfval  25798  plyeq0lem  26115  taylfval  26266  ulmval  26289  dmarea  26867  dchrplusg  27158  madefi  27824  addsval  27869  mulsval  28012  zsex  28268  tgjustc1  28402  tgjustc2  28403  iscgrg  28439  ishlg  28529  ishpg  28686  iscgra  28736  isinag  28765  isleag  28774  axlowdimlem15  28883  axlowdim  28888  isgrpoi  30427  sspval  30652  0ofval  30716  ajfval  30738  hvmulex  30940  gsumwrd2dccat  33007  inftmrel  33134  isinftm  33135  smatrcl  33786  tpr2rico  33902  faeval  34236  mbfmco2  34256  br2base  34260  sxbrsigalem0  34262  sxbrsigalem3  34263  dya2iocrfn  34270  dya2iocct  34271  dya2iocnrect  34272  dya2iocuni  34274  dya2iocucvr  34275  sxbrsigalem2  34277  eulerpartlemgs2  34371  ccatmulgnn0dir  34533  afsval  34662  cvmlift2lem9  35298  satfv0  35345  satf00  35361  prv1n  35418  mexval  35489  mdvval  35491  mpstval  35522  brimg  35925  brrestrict  35937  colinearex  36048  poimirlem4  37618  poimirlem28  37642  mblfinlem1  37651  heiborlem3  37807  rrnval  37821  ismrer1  37832  dfcnvrefrels2  38519  dfcnvrefrels3  38520  lcvfbr  39013  cmtfvalN  39203  cvrfval  39261  dvhvbase  41081  dvhfvadd  41085  dvhfvsca  41094  dibval  41136  dibfna  41148  dicval  41170  hdmap1fval  41790  ltex  42233  leex  42234  subex  42235  evlsvvval  42551  mzpincl  42722  pellexlem3  42819  pellexlem4  42820  pellexlem5  42821  aomclem6  43048  trclexi  43609  rtrclexi  43610  brtrclfv2  43716  mnringmulrcld  44217  hoiprodcl2  46553  hoicvrrex  46554  ovn0lem  46563  ovnhoilem1  46599  ovnlecvr2  46608  opnvonmbllem1  46630  opnvonmbllem2  46631  ovolval2lem  46641  ovolval2  46642  ovolval3  46645  ovolval4lem2  46648  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  smflimlem6  46774  gpgvtx  48034  gpgiedg  48035  sectfn  49018  nelsubc3  49060  cofidvala  49105  cofidval  49108  diag1f1lem  49295  fucoelvv  49309  fucofvalne  49314  functhinclem1  49433  functhinclem3  49435  functermc2  49498  idfudiag1bas  49513  idfudiag1  49514  prstchomval  49548  elpglem3  49702  pgindnf  49705  aacllem  49790