Theorem xpex 7708

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442   × cxp 5630

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 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-opab 5163  df-xp 5638  df-rel 5639

This theorem is referenced by:  oprabex  7930  oprabex3  7931  mpoexw  8032  naddcllem  8614  fnpm  8783  mapsnf1o2  8844  ixpsnf1o  8888  xpsnen  9001  endisj  9004  xpcomen  9008  xpassen  9011  xpmapenlem  9084  unxpdomlem3  9170  hartogslem1  9459  rankxpl  9799  rankfu  9801  rankmapu  9802  rankxplim  9803  rankxplim2  9804  rankxplim3  9805  rankxpsuc  9806  r0weon  9934  infxpenlem  9935  infxpenc2lem2  9942  dfac3  10043  dfac5lem2  10046  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  unctb  10126  axcc2lem  10358  axdc3lem  10372  axdc4lem  10377  enqex  10845  nqex  10846  nrex1  10987  enrex  10990  axcnex  11070  zexALT  12520  cnexALT  12911  mpoaddex  12913  addex  12914  mpomulex  12915  mulex  12916  ixxex  13284  shftfval  15005  climconst2  15483  cpnnen  16166  ruclem13  16179  cnso  16184  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdsle  17394  prdshom  17399  prdsco  17400  xrsle  17537  fnmrc  17542  mrcfval  17543  mreacs  17593  comfffval  17633  oppccofval  17651  sectfval  17687  brssc  17750  sscpwex  17751  isssc  17756  isfunc  17800  isfuncd  17801  idfu2nd  17813  idfu1st  17815  idfucl  17817  wunfunc  17837  fuccofval  17898  homafval  17965  homaf  17966  homaval  17967  coapm  18007  catccofval  18040  catcfuccl  18054  xpcval  18112  xpcbas  18113  xpchom  18115  xpccofval  18117  1stfval  18126  2ndfval  18129  1stfcl  18132  2ndfcl  18133  catcxpccl  18142  evlf2  18153  evlf1  18155  evlfcl  18157  hof1fval  18188  hof2fval  18190  hofcl  18194  ipoval  18465  letsr  18528  frmdplusg  18791  eqgfval  19117  efglem  19657  efgval  19658  cnfldds  21333  cnfldfun  21335  cnfldfunALT  21336  cnflddsOLD  21346  cnfldfunOLD  21348  cnfldfunALTOLD  21349  xrsadd  21352  xrsmul  21353  xrsds  21376  pzriprnglem13  21460  pzriprnglem14  21461  znle  21503  pjfval  21673  psrplusg  21904  ltbval  22010  opsrle  22014  evlslem2  22046  evlsvvval  22060  evlssca  22061  mpfind  22082  psdmul  22121  evls1sca  22279  pf1ind  22311  mat1dimmul  22432  2ndcctbss  23411  txuni2  23521  txbas  23523  eltx  23524  txcnp  23576  txcnmpt  23580  txrest  23587  txlm  23604  tx1stc  23606  tx2ndc  23607  txkgen  23608  txflf  23962  cnextfval  24018  distgp  24055  indistgp  24056  ustfn  24158  ustn0  24177  ussid  24216  ressuss  24218  ishtpy  24939  isphtpc  24961  elovolmlem  25443  dyadmbl  25569  vitali  25582  mbfimaopnlem  25624  dvfval  25866  plyeq0lem  26183  taylfval  26334  ulmval  26357  dmarea  26935  dchrplusg  27226  madefi  27921  addsval  27970  mulsval  28117  zsex  28388  tgjustc1  28559  tgjustc2  28560  iscgrg  28596  ishlg  28686  ishpg  28843  iscgra  28893  isinag  28922  isleag  28931  axlowdimlem15  29041  axlowdim  29046  isgrpoi  30585  sspval  30810  0ofval  30874  ajfval  30896  hvmulex  31098  gsumwrd2dccat  33171  inftmrel  33273  isinftm  33274  smatrcl  33973  tpr2rico  34089  faeval  34423  mbfmco2  34442  br2base  34446  sxbrsigalem0  34448  sxbrsigalem3  34449  dya2iocrfn  34456  dya2iocct  34457  dya2iocnrect  34458  dya2iocuni  34460  dya2iocucvr  34461  sxbrsigalem2  34463  eulerpartlemgs2  34557  ccatmulgnn0dir  34719  afsval  34848  cvmlift2lem9  35524  satfv0  35571  satf00  35587  prv1n  35644  mexval  35715  mdvval  35717  mpstval  35748  brimg  36148  brrestrict  36162  colinearex  36273  poimirlem4  37869  poimirlem28  37893  mblfinlem1  37902  heiborlem3  38058  rrnval  38072  ismrer1  38083  dfcnvrefrels2  38853  dfcnvrefrels3  38854  lcvfbr  39390  cmtfvalN  39580  cvrfval  39638  dvhvbase  41457  dvhfvadd  41461  dvhfvsca  41470  dibval  41512  dibfna  41524  dicval  41546  hdmap1fval  42166  ltex  42609  leex  42610  subex  42611  mzpincl  43085  pellexlem3  43182  pellexlem4  43183  pellexlem5  43184  aomclem6  43410  trclexi  43970  rtrclexi  43971  brtrclfv2  44077  mnringmulrcld  44578  hoiprodcl2  46907  hoicvrrex  46908  ovn0lem  46917  ovnhoilem1  46953  ovnlecvr2  46962  opnvonmbllem1  46984  opnvonmbllem2  46985  ovolval2lem  46995  ovolval2  46996  ovolval3  46999  ovolval4lem2  47002  ovolval5lem2  47005  ovnovollem1  47008  ovnovollem2  47009  smflimlem6  47128  gpgvtx  48397  gpgiedg  48398  sectfn  49382  nelsubc3  49424  cofidvala  49469  cofidval  49472  diag1f1lem  49659  fucoelvv  49673  fucofvalne  49678  functhinclem1  49797  functhinclem3  49799  functermc2  49862  idfudiag1bas  49877  idfudiag1  49878  prstchomval  49912  elpglem3  50066  pgindnf  50069  aacllem  50154