Theorem xpex 7794

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   × cxp 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pow 5332  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-opab 5172  df-xp 5662  df-rel 5663

This theorem is used by:  oprabex  8015  oprabex3  8016  mpoexw  8119  naddcllem  8716  fnpm  8885  mapsnf1o2  8953  ixpsnf1o  8997  xpsnen  9111  endisj  9114  xpcomen  9118  xpassen  9121  xpmapenlem  9194  unxpdomlem3  9280  hartogslem1  9566  rankxpl  9922  rankfu  9924  rankmapu  9925  rankxplim  9926  rankxplim2  9927  rankxplim3  9928  rankxpsuc  9929  r0weon  10121  infxpenlem  10122  infxpenc2lem2  10129  dfac3  10230  dfac5lem2  10233  dfac5lem3  10234  dfac5lem4  10235  unctb  10312  axcc2lem  10544  axdc3lem  10558  axdc4lem  10563  enqex  11037  nqex  11038  nrex1  11179  enrex  11182  axcnex  11262  zexALT  12743  cnexALT  13144  mpoaddex  13146  addex  13147  mpomulex  13148  mulex  13149  ixxex  13517  shftfval  15255  climconst2  15747  cpnnen  16429  ruclem13  16442  cnso  16447  prdsplusg  17661  prdsmulr  17662  prdsvsca  17663  prdsle  17665  prdshom  17670  prdsco  17671  xrsle  17808  fnmrc  17813  mrcfval  17814  mreacs  17864  comfffval  17904  oppccofval  17922  sectfval  17958  brssc  18021  sscpwex  18022  isssc  18027  isfunc  18071  isfuncd  18072  idfu2nd  18084  idfu1st  18086  idfucl  18088  wunfunc  18108  fuccofval  18169  homafval  18236  homaf  18237  homaval  18238  coapm  18278  catccofval  18311  catcfuccl  18325  xpcval  18383  xpcbas  18384  xpchom  18386  xpccofval  18388  1stfval  18397  2ndfval  18400  1stfcl  18403  2ndfcl  18404  catcxpccl  18413  evlf2  18424  evlf1  18426  evlfcl  18428  hof1fval  18459  hof2fval  18461  hofcl  18465  ipoval  18736  letsr  18799  frmdplusg  19082  smndex1gbas  19130  smndex1gid  19132  smndex1igid  19134  eqgfval  19420  efglem  19963  efgval  19964  cnfldds  21723  cnfldfun  21725  cnfldfunALT  21726  xrsadd  21729  xrsmul  21730  xrsds  21749  pzriprnglem13  21832  pzriprnglem14  21833  znle  21875  pjfval  22045  psrplusg  22278  ltbval  22385  opsrle  22389  evlslem2  22421  evlsvvval  22435  evlssca  22436  mpfind  22457  psdmul  22520  evls1sca  22674  pf1ind  22706  mat1dimmul  22824  2ndcctbss  23807  txuni2  23917  txbas  23919  eltx  23920  txcnp  23972  txcnmpt  23976  txrest  23983  txlm  24000  tx1stc  24002  tx2ndc  24003  txkgen  24004  txflf  24358  cnextfval  24414  distgp  24451  indistgp  24452  ustfn  24554  ustn0  24573  ussid  24612  ressuss  24614  ishtpy  25326  isphtpc  25348  elovolmlem  25828  dyadmbl  25954  vitali  25967  mbfimaopnlem  26009  dvfval  26250  plyeq0lem  26562  taylfval  26719  ulmval  26740  dmarea  27318  dchrplusg  27607  addsval  28381  mulsval  28528  zsex  28799  istrkg2ld  28955  tgjustc1  28970  tgjustc2  28971  iscgrg  29008  ishlg2  29098  ishlg  29101  ishpg  29270  iscgra  29349  isinag  29390  isleag  29399  axlowdimlem15  29567  axlowdim  29572  isgrpoi  31133  sspval  31358  0ofval  31422  ajfval  31444  hvmulex  31646  padct  33384  gsumwrd2dccat  33715  inftmrel  33817  isinftm  33818  smatrcl  34511  tpr2rico  34627  faeval  34962  mbfmco2  34980  br2base  34984  sxbrsigalem0  34986  sxbrsigalem3  34987  dya2iocrfn  34994  dya2iocct  34995  dya2iocnrect  34996  dya2iocuni  34998  dya2iocucvr  34999  sxbrsigalem2  35001  eulerpartlemgs2  35095  ccatmulgnn0dir  35257  afsval  35386  dfac15  35858  vonf1onprcf1ac  36057  cvmlift2lem9  36256  satfv0  36303  satf00  36319  prv1n  36376  mexval  36447  mdvval  36449  mpstval  36480  brimg  36890  brrestrict  36904  colinearex  37016  nmulprop  37130  poimirlem4  38747  poimirlem28  38771  mblfinlem1  38780  heiborlem3  38950  rrnval  38964  ismrer1  38975  dfcnvrefrels2  39743  dfcnvrefrels3  39744  lcvfbr  40280  cmtfvalN  40470  cvrfval  40528  dvhvbase  42347  dvhfvadd  42351  dvhfvsca  42360  dibval  42402  dibfna  42414  dicval  42436  hdmap1fval  43056  ltex  43500  leex  43501  subex  43502  mzpincl  43949  pellexlem3  44042  pellexlem4  44043  pellexlem5  44044  aomclem6  44265  trclexi  44823  rtrclexi  44824  brtrclfv2  44930  mnringmulrcld  45429  mpoexwd  46129  grpgimcanon  46134  hoiprodcl2  47780  hoicvrrex  47781  ovn0lem  47790  ovnhoilem1  47826  ovnlecvr2  47835  opnvonmbllem1  47857  opnvonmbllem2  47858  ovolval2lem  47868  ovolval2  47869  ovolval3  47872  ovolval4lem2  47875  ovolval5lem2  47878  ovnovollem1  47881  ovnovollem2  47882  gpgvtx  49356  gpgiedg  49357  sectfn  50358  nelsubc3  50400  cofidvala  50447  cofidval  50450  diag1f1lem  50643  fucoelvv  50657  fucofvalne  50662  functhinclem1  50794  functhinclem3  50796  functermc2  50859  idfudiag1bas  50874  idfudiag1  50875  prstchomval  50912  parcatid2  50978  parcatid  50979  par2str  50984  elpglem3  51096  pgindnf  51099  aacllem  51251