Theorem xpex 7773

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  oprabex  8001  oprabex3  8002  mpoexw  8103  naddcllem  8714  fnpm  8874  mapsnf1o2  8934  ixpsnf1o  8978  xpsnen  9095  endisj  9098  xpcomen  9103  xpassen  9106  xpmapenlem  9184  unxpdomlem3  9288  hartogslem1  9582  rankxpl  9915  rankfu  9917  rankmapu  9918  rankxplim  9919  rankxplim2  9920  rankxplim3  9921  rankxpsuc  9922  r0weon  10052  infxpenlem  10053  infxpenc2lem2  10060  dfac3  10161  dfac5lem2  10164  dfac5lem3  10165  dfac5lem4  10166  dfac5lem4OLD  10168  unctb  10244  axcc2lem  10476  axdc3lem  10490  axdc4lem  10495  enqex  10962  nqex  10963  nrex1  11104  enrex  11107  axcnex  11187  zexALT  12633  cnexALT  13028  mpoaddex  13030  addex  13031  mpomulex  13032  mulex  13033  ixxex  13398  shftfval  15109  climconst2  15584  cpnnen  16265  ruclem13  16278  cnso  16283  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdsle  17507  prdshom  17512  prdsco  17513  fnmrc  17650  mrcfval  17651  mreacs  17701  comfffval  17741  oppccofval  17759  sectfval  17795  brssc  17858  sscpwex  17859  isssc  17864  isfunc  17909  isfuncd  17910  idfu2nd  17922  idfu1st  17924  idfucl  17926  wunfunc  17946  fuccofval  18007  homafval  18074  homaf  18075  homaval  18076  coapm  18116  catccofval  18149  catcfuccl  18163  xpcval  18222  xpcbas  18223  xpchom  18225  xpccofval  18227  1stfval  18236  2ndfval  18239  1stfcl  18242  2ndfcl  18243  catcxpccl  18252  evlf2  18263  evlf1  18265  evlfcl  18267  hof1fval  18298  hof2fval  18300  hofcl  18304  ipoval  18575  letsr  18638  frmdplusg  18867  eqgfval  19194  efglem  19734  efgval  19735  cnfldds  21376  cnfldfun  21378  cnfldfunALT  21379  cnflddsOLD  21389  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  xrsadd  21397  xrsmul  21398  xrsle  21400  xrsds  21427  pzriprnglem13  21504  pzriprnglem14  21505  znle  21551  pjfval  21726  psrplusg  21956  ltbval  22061  opsrle  22065  evlslem2  22103  evlssca  22113  mpfind  22131  psdmul  22170  evls1sca  22327  pf1ind  22359  mat1dimmul  22482  2ndcctbss  23463  txuni2  23573  txbas  23575  eltx  23576  txcnp  23628  txcnmpt  23632  txrest  23639  txlm  23656  tx1stc  23658  tx2ndc  23659  txkgen  23660  txflf  24014  cnextfval  24070  distgp  24107  indistgp  24108  ustfn  24210  ustn0  24229  ussid  24269  ressuss  24271  ishtpy  25004  isphtpc  25026  elovolmlem  25509  dyadmbl  25635  vitali  25648  mbfimaopnlem  25690  dvfval  25932  plyeq0lem  26249  taylfval  26400  ulmval  26423  dmarea  27000  dchrplusg  27291  madefi  27950  addsval  27995  mulsval  28135  zsex  28366  tgjustc1  28483  tgjustc2  28484  iscgrg  28520  ishlg  28610  ishpg  28767  iscgra  28817  isinag  28846  isleag  28855  axlowdimlem15  28971  axlowdim  28976  isgrpoi  30517  sspval  30742  0ofval  30806  ajfval  30828  hvmulex  31030  gsumwrd2dccat  33070  inftmrel  33187  isinftm  33188  smatrcl  33795  tpr2rico  33911  faeval  34247  mbfmco2  34267  br2base  34271  sxbrsigalem0  34273  sxbrsigalem3  34274  dya2iocrfn  34281  dya2iocct  34282  dya2iocnrect  34283  dya2iocuni  34285  dya2iocucvr  34286  sxbrsigalem2  34288  eulerpartlemgs2  34382  ccatmulgnn0dir  34557  afsval  34686  cvmlift2lem9  35316  satfv0  35363  satf00  35379  prv1n  35436  mexval  35507  mdvval  35509  mpstval  35540  brimg  35938  brrestrict  35950  colinearex  36061  poimirlem4  37631  poimirlem28  37655  mblfinlem1  37664  heiborlem3  37820  rrnval  37834  ismrer1  37845  dfcnvrefrels2  38529  dfcnvrefrels3  38530  lcvfbr  39021  cmtfvalN  39211  cvrfval  39269  dvhvbase  41089  dvhfvadd  41093  dvhfvsca  41102  dibval  41144  dibfna  41156  dicval  41178  hdmap1fval  41798  ltex  42286  leex  42287  subex  42288  evlsvvval  42573  mzpincl  42745  pellexlem3  42842  pellexlem4  42843  pellexlem5  42844  aomclem6  43071  trclexi  43633  rtrclexi  43634  brtrclfv2  43740  mnringmulrcld  44247  hoiprodcl2  46570  hoicvrrex  46571  ovn0lem  46580  ovnhoilem1  46616  ovnlecvr2  46625  opnvonmbllem1  46647  opnvonmbllem2  46648  ovolval2lem  46658  ovolval2  46659  ovolval3  46662  ovolval4lem2  46665  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  smflimlem6  46791  gpgvtx  48002  gpgiedg  48003  fucoelvv  49015  fucofvalne  49020  functhinclem1  49093  functhinclem3  49095  functermc2  49141  prstchomval  49163  elpglem3  49232  pgindnf  49235  aacllem  49320