Theorem xpex 7740

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-opab 5212  df-xp 5683  df-rel 5684

This theorem is referenced by:  oprabex  7963  oprabex3  7964  mpoexw  8065  naddcllem  8675  fnpm  8828  mapsnf1o2  8888  ixpsnf1o  8932  xpsnen  9055  endisj  9058  xpcomen  9063  xpassen  9066  xpmapenlem  9144  unxpdomlem3  9252  hartogslem1  9537  rankxpl  9870  rankfu  9872  rankmapu  9873  rankxplim  9874  rankxplim2  9875  rankxplim3  9876  rankxpsuc  9877  r0weon  10007  infxpenlem  10008  infxpenc2lem2  10015  dfac3  10116  dfac5lem2  10119  dfac5lem3  10120  dfac5lem4  10121  unctb  10200  axcc2lem  10431  axdc3lem  10445  axdc4lem  10450  enqex  10917  nqex  10918  nrex1  11059  enrex  11062  axcnex  11142  zexALT  12578  cnexALT  12970  addex  12972  mulex  12973  ixxex  13335  shftfval  15017  climconst2  15492  cpnnen  16172  ruclem13  16185  cnso  16190  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdsle  17408  prdshom  17413  prdsco  17414  fnmrc  17551  mrcfval  17552  mreacs  17602  comfffval  17642  oppccofval  17661  sectfval  17698  brssc  17761  sscpwex  17762  isssc  17767  isfunc  17814  isfuncd  17815  idfu2nd  17827  idfu1st  17829  idfucl  17831  wunfunc  17849  wunfuncOLD  17850  fuccofval  17911  homafval  17979  homaf  17980  homaval  17981  coapm  18021  catccofval  18054  catcfuccl  18069  catcfucclOLD  18070  xpcval  18129  xpcbas  18130  xpchom  18132  xpccofval  18134  1stfval  18143  2ndfval  18146  1stfcl  18149  2ndfcl  18150  catcxpccl  18159  catcxpcclOLD  18160  evlf2  18171  evlf1  18173  evlfcl  18175  hof1fval  18206  hof2fval  18208  hofcl  18212  ipoval  18483  letsr  18546  frmdplusg  18735  eqgfval  19056  efglem  19584  efgval  19585  cnfldds  20954  cnfldfun  20956  cnfldfunALT  20957  cnfldfunALTOLD  20958  xrsadd  20962  xrsmul  20963  xrsle  20965  xrsds  20988  znle  21088  pjfval  21261  psrplusg  21500  ltbval  21598  opsrle  21602  evlslem2  21642  evlssca  21652  mpfind  21670  evls1sca  21842  pf1ind  21874  mat1dimmul  21978  2ndcctbss  22959  txuni2  23069  txbas  23071  eltx  23072  txcnp  23124  txcnmpt  23128  txrest  23135  txlm  23152  tx1stc  23154  tx2ndc  23155  txkgen  23156  txflf  23510  cnextfval  23566  distgp  23603  indistgp  23604  ustfn  23706  ustn0  23725  ussid  23765  ressuss  23767  ishtpy  24488  isphtpc  24510  elovolmlem  24991  dyadmbl  25117  vitali  25130  mbfimaopnlem  25172  dvfval  25414  plyeq0lem  25724  taylfval  25871  ulmval  25892  dmarea  26462  dchrplusg  26750  addsval  27446  mulsval  27565  tgjustc1  27726  tgjustc2  27727  iscgrg  27763  ishlg  27853  ishpg  28010  iscgra  28060  isinag  28089  isleag  28098  axlowdimlem15  28214  axlowdim  28219  isgrpoi  29751  sspval  29976  0ofval  30040  ajfval  30062  hvmulex  30264  inftmrel  32326  isinftm  32327  smatrcl  32776  tpr2rico  32892  faeval  33244  mbfmco2  33264  br2base  33268  sxbrsigalem0  33270  sxbrsigalem3  33271  dya2iocrfn  33278  dya2iocct  33279  dya2iocnrect  33280  dya2iocuni  33282  dya2iocucvr  33283  sxbrsigalem2  33285  eulerpartlemgs2  33379  ccatmulgnn0dir  33553  afsval  33683  cvmlift2lem9  34302  satfv0  34349  satf00  34365  prv1n  34422  mexval  34493  mdvval  34495  mpstval  34526  brimg  34909  brrestrict  34921  colinearex  35032  poimirlem4  36492  poimirlem28  36516  mblfinlem1  36525  heiborlem3  36681  rrnval  36695  ismrer1  36706  dfcnvrefrels2  37398  dfcnvrefrels3  37399  lcvfbr  37890  cmtfvalN  38080  cvrfval  38138  dvhvbase  39958  dvhfvadd  39962  dvhfvsca  39971  dibval  40013  dibfna  40025  dicval  40047  hdmap1fval  40667  evlsvvval  41135  mzpincl  41472  pellexlem3  41569  pellexlem4  41570  pellexlem5  41571  aomclem6  41801  trclexi  42371  rtrclexi  42372  brtrclfv2  42478  mnringmulrcld  42987  hoiprodcl2  45271  hoicvrrex  45272  ovn0lem  45281  ovnhoilem1  45317  ovnlecvr2  45326  opnvonmbllem1  45348  opnvonmbllem2  45349  ovolval2lem  45359  ovolval2  45360  ovolval3  45363  ovolval4lem2  45366  ovolval5lem2  45369  ovnovollem1  45372  ovnovollem2  45373  smflimlem6  45492  pzriprnglem13  46817  pzriprnglem14  46818  functhinclem1  47661  functhinclem3  47663  prstchomval  47694  elpglem3  47758  pgindnf  47761  aacllem  47848