Theorem xpex 7744

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

Syntax hints:   ∈ wcel 2105  Vcvv 3473   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  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  7967  oprabex3  7968  mpoexw  8069  naddcllem  8681  fnpm  8834  mapsnf1o2  8894  ixpsnf1o  8938  xpsnen  9061  endisj  9064  xpcomen  9069  xpassen  9072  xpmapenlem  9150  unxpdomlem3  9258  hartogslem1  9543  rankxpl  9876  rankfu  9878  rankmapu  9879  rankxplim  9880  rankxplim2  9881  rankxplim3  9882  rankxpsuc  9883  r0weon  10013  infxpenlem  10014  infxpenc2lem2  10021  dfac3  10122  dfac5lem2  10125  dfac5lem3  10126  dfac5lem4  10127  unctb  10206  axcc2lem  10437  axdc3lem  10451  axdc4lem  10456  enqex  10923  nqex  10924  nrex1  11065  enrex  11068  axcnex  11148  zexALT  12585  cnexALT  12977  addex  12979  mulex  12980  ixxex  13342  shftfval  15024  climconst2  15499  cpnnen  16179  ruclem13  16192  cnso  16197  prdsplusg  17411  prdsmulr  17412  prdsvsca  17413  prdsle  17415  prdshom  17420  prdsco  17421  fnmrc  17558  mrcfval  17559  mreacs  17609  comfffval  17649  oppccofval  17668  sectfval  17705  brssc  17768  sscpwex  17769  isssc  17774  isfunc  17821  isfuncd  17822  idfu2nd  17834  idfu1st  17836  idfucl  17838  wunfunc  17856  wunfuncOLD  17857  fuccofval  17918  homafval  17986  homaf  17987  homaval  17988  coapm  18028  catccofval  18061  catcfuccl  18076  catcfucclOLD  18077  xpcval  18136  xpcbas  18137  xpchom  18139  xpccofval  18141  1stfval  18150  2ndfval  18153  1stfcl  18156  2ndfcl  18157  catcxpccl  18166  catcxpcclOLD  18167  evlf2  18178  evlf1  18180  evlfcl  18182  hof1fval  18213  hof2fval  18215  hofcl  18219  ipoval  18490  letsr  18553  frmdplusg  18774  eqgfval  19096  efglem  19629  efgval  19630  cnfldds  21158  cnfldfun  21160  cnfldfunALT  21161  cnfldfunALTOLD  21162  xrsadd  21166  xrsmul  21167  xrsle  21169  xrsds  21192  pzriprnglem13  21266  pzriprnglem14  21267  znle  21311  pjfval  21484  psrplusg  21723  ltbval  21822  opsrle  21826  evlslem2  21866  evlssca  21876  mpfind  21894  evls1sca  22075  pf1ind  22107  mat1dimmul  22211  2ndcctbss  23192  txuni2  23302  txbas  23304  eltx  23305  txcnp  23357  txcnmpt  23361  txrest  23368  txlm  23385  tx1stc  23387  tx2ndc  23388  txkgen  23389  txflf  23743  cnextfval  23799  distgp  23836  indistgp  23837  ustfn  23939  ustn0  23958  ussid  23998  ressuss  24000  ishtpy  24731  isphtpc  24753  elovolmlem  25236  dyadmbl  25362  vitali  25375  mbfimaopnlem  25417  dvfval  25659  plyeq0lem  25973  taylfval  26121  ulmval  26142  dmarea  26713  dchrplusg  27001  addsval  27699  mulsval  27819  tgjustc1  28008  tgjustc2  28009  iscgrg  28045  ishlg  28135  ishpg  28292  iscgra  28342  isinag  28371  isleag  28380  axlowdimlem15  28496  axlowdim  28501  isgrpoi  30033  sspval  30258  0ofval  30322  ajfval  30344  hvmulex  30546  inftmrel  32611  isinftm  32612  smatrcl  33089  tpr2rico  33205  faeval  33557  mbfmco2  33577  br2base  33581  sxbrsigalem0  33583  sxbrsigalem3  33584  dya2iocrfn  33591  dya2iocct  33592  dya2iocnrect  33593  dya2iocuni  33595  dya2iocucvr  33596  sxbrsigalem2  33598  eulerpartlemgs2  33692  ccatmulgnn0dir  33866  afsval  33996  cvmlift2lem9  34615  satfv0  34662  satf00  34678  prv1n  34735  mexval  34806  mdvval  34808  mpstval  34839  brimg  35228  brrestrict  35240  colinearex  35351  mpomulex  35478  mpoaddex  35485  gg-cnfldds  35494  gg-cnfldfun  35496  gg-cnfldfunALT  35497  poimirlem4  36808  poimirlem28  36832  mblfinlem1  36841  heiborlem3  36997  rrnval  37011  ismrer1  37022  dfcnvrefrels2  37714  dfcnvrefrels3  37715  lcvfbr  38206  cmtfvalN  38396  cvrfval  38454  dvhvbase  40274  dvhfvadd  40278  dvhfvsca  40287  dibval  40329  dibfna  40341  dicval  40363  hdmap1fval  40983  evlsvvval  41450  mzpincl  41787  pellexlem3  41884  pellexlem4  41885  pellexlem5  41886  aomclem6  42116  trclexi  42686  rtrclexi  42687  brtrclfv2  42793  mnringmulrcld  43302  hoiprodcl2  45582  hoicvrrex  45583  ovn0lem  45592  ovnhoilem1  45628  ovnlecvr2  45637  opnvonmbllem1  45659  opnvonmbllem2  45660  ovolval2lem  45670  ovolval2  45671  ovolval3  45674  ovolval4lem2  45677  ovolval5lem2  45680  ovnovollem1  45683  ovnovollem2  45684  smflimlem6  45803  functhinclem1  47761  functhinclem3  47763  prstchomval  47794  elpglem3  47858  pgindnf  47861  aacllem  47948