Theorem xpex 7686

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   × cxp 5614

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-opab 5154  df-xp 5622  df-rel 5623

This theorem is referenced by:  oprabex  7908  oprabex3  7909  mpoexw  8010  naddcllem  8591  fnpm  8758  mapsnf1o2  8818  ixpsnf1o  8862  xpsnen  8974  endisj  8977  xpcomen  8981  xpassen  8984  xpmapenlem  9057  unxpdomlem3  9142  hartogslem1  9428  rankxpl  9765  rankfu  9767  rankmapu  9768  rankxplim  9769  rankxplim2  9770  rankxplim3  9771  rankxpsuc  9772  r0weon  9900  infxpenlem  9901  infxpenc2lem2  9908  dfac3  10009  dfac5lem2  10012  dfac5lem3  10013  dfac5lem4  10014  dfac5lem4OLD  10016  unctb  10092  axcc2lem  10324  axdc3lem  10338  axdc4lem  10343  enqex  10810  nqex  10811  nrex1  10952  enrex  10955  axcnex  11035  zexALT  12485  cnexALT  12881  mpoaddex  12883  addex  12884  mpomulex  12885  mulex  12886  ixxex  13253  shftfval  14974  climconst2  15452  cpnnen  16135  ruclem13  16148  cnso  16153  prdsplusg  17359  prdsmulr  17360  prdsvsca  17361  prdsle  17363  prdshom  17368  prdsco  17369  xrsle  17505  fnmrc  17510  mrcfval  17511  mreacs  17561  comfffval  17601  oppccofval  17619  sectfval  17655  brssc  17718  sscpwex  17719  isssc  17724  isfunc  17768  isfuncd  17769  idfu2nd  17781  idfu1st  17783  idfucl  17785  wunfunc  17805  fuccofval  17866  homafval  17933  homaf  17934  homaval  17935  coapm  17975  catccofval  18008  catcfuccl  18022  xpcval  18080  xpcbas  18081  xpchom  18083  xpccofval  18085  1stfval  18094  2ndfval  18097  1stfcl  18100  2ndfcl  18101  catcxpccl  18110  evlf2  18121  evlf1  18123  evlfcl  18125  hof1fval  18156  hof2fval  18158  hofcl  18162  ipoval  18433  letsr  18496  frmdplusg  18759  eqgfval  19086  efglem  19626  efgval  19627  cnfldds  21301  cnfldfun  21303  cnfldfunALT  21304  cnflddsOLD  21314  cnfldfunOLD  21316  cnfldfunALTOLD  21317  xrsadd  21320  xrsmul  21321  xrsds  21344  pzriprnglem13  21428  pzriprnglem14  21429  znle  21471  pjfval  21641  psrplusg  21871  ltbval  21976  opsrle  21980  evlslem2  22012  evlssca  22022  mpfind  22040  psdmul  22079  evls1sca  22236  pf1ind  22268  mat1dimmul  22389  2ndcctbss  23368  txuni2  23478  txbas  23480  eltx  23481  txcnp  23533  txcnmpt  23537  txrest  23544  txlm  23561  tx1stc  23563  tx2ndc  23564  txkgen  23565  txflf  23919  cnextfval  23975  distgp  24012  indistgp  24013  ustfn  24115  ustn0  24134  ussid  24173  ressuss  24175  ishtpy  24896  isphtpc  24918  elovolmlem  25400  dyadmbl  25526  vitali  25539  mbfimaopnlem  25581  dvfval  25823  plyeq0lem  26140  taylfval  26291  ulmval  26314  dmarea  26892  dchrplusg  27183  madefi  27856  addsval  27903  mulsval  28046  zsex  28302  tgjustc1  28451  tgjustc2  28452  iscgrg  28488  ishlg  28578  ishpg  28735  iscgra  28785  isinag  28814  isleag  28823  axlowdimlem15  28932  axlowdim  28937  isgrpoi  30473  sspval  30698  0ofval  30762  ajfval  30784  hvmulex  30986  gsumwrd2dccat  33042  inftmrel  33144  isinftm  33145  smatrcl  33804  tpr2rico  33920  faeval  34254  mbfmco2  34273  br2base  34277  sxbrsigalem0  34279  sxbrsigalem3  34280  dya2iocrfn  34287  dya2iocct  34288  dya2iocnrect  34289  dya2iocuni  34291  dya2iocucvr  34292  sxbrsigalem2  34294  eulerpartlemgs2  34388  ccatmulgnn0dir  34550  afsval  34679  cvmlift2lem9  35343  satfv0  35390  satf00  35406  prv1n  35463  mexval  35534  mdvval  35536  mpstval  35567  brimg  35970  brrestrict  35982  colinearex  36093  poimirlem4  37663  poimirlem28  37687  mblfinlem1  37696  heiborlem3  37852  rrnval  37866  ismrer1  37877  dfcnvrefrels2  38564  dfcnvrefrels3  38565  lcvfbr  39058  cmtfvalN  39248  cvrfval  39306  dvhvbase  41125  dvhfvadd  41129  dvhfvsca  41138  dibval  41180  dibfna  41192  dicval  41214  hdmap1fval  41834  ltex  42277  leex  42278  subex  42279  evlsvvval  42595  mzpincl  42766  pellexlem3  42863  pellexlem4  42864  pellexlem5  42865  aomclem6  43091  trclexi  43652  rtrclexi  43653  brtrclfv2  43759  mnringmulrcld  44260  hoiprodcl2  46592  hoicvrrex  46593  ovn0lem  46602  ovnhoilem1  46638  ovnlecvr2  46647  opnvonmbllem1  46669  opnvonmbllem2  46670  ovolval2lem  46680  ovolval2  46681  ovolval3  46684  ovolval4lem2  46687  ovolval5lem2  46690  ovnovollem1  46693  ovnovollem2  46694  smflimlem6  46813  gpgvtx  48073  gpgiedg  48074  sectfn  49060  nelsubc3  49102  cofidvala  49147  cofidval  49150  diag1f1lem  49337  fucoelvv  49351  fucofvalne  49356  functhinclem1  49475  functhinclem3  49477  functermc2  49540  idfudiag1bas  49555  idfudiag1  49556  prstchomval  49590  elpglem3  49744  pgindnf  49747  aacllem  49832