Theorem xpex 7698

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   × cxp 5620

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 5231  ax-pow 5300  ax-pr 5368  ax-un 7680

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-opab 5149  df-xp 5628  df-rel 5629

This theorem is referenced by:  oprabex  7920  oprabex3  7921  mpoexw  8022  naddcllem  8603  fnpm  8772  mapsnf1o2  8833  ixpsnf1o  8877  xpsnen  8990  endisj  8993  xpcomen  8997  xpassen  9000  xpmapenlem  9073  unxpdomlem3  9159  hartogslem1  9448  rankxpl  9788  rankfu  9790  rankmapu  9791  rankxplim  9792  rankxplim2  9793  rankxplim3  9794  rankxpsuc  9795  r0weon  9923  infxpenlem  9924  infxpenc2lem2  9931  dfac3  10032  dfac5lem2  10035  dfac5lem3  10036  dfac5lem4  10037  dfac5lem4OLD  10039  unctb  10115  axcc2lem  10347  axdc3lem  10361  axdc4lem  10366  enqex  10834  nqex  10835  nrex1  10976  enrex  10979  axcnex  11059  zexALT  12533  cnexALT  12925  mpoaddex  12927  addex  12928  mpomulex  12929  mulex  12930  ixxex  13298  shftfval  15021  climconst2  15499  cpnnen  16185  ruclem13  16198  cnso  16203  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  prdsle  17414  prdshom  17419  prdsco  17420  xrsle  17557  fnmrc  17562  mrcfval  17563  mreacs  17613  comfffval  17653  oppccofval  17671  sectfval  17707  brssc  17770  sscpwex  17771  isssc  17776  isfunc  17820  isfuncd  17821  idfu2nd  17833  idfu1st  17835  idfucl  17837  wunfunc  17857  fuccofval  17918  homafval  17985  homaf  17986  homaval  17987  coapm  18027  catccofval  18060  catcfuccl  18074  xpcval  18132  xpcbas  18133  xpchom  18135  xpccofval  18137  1stfval  18146  2ndfval  18149  1stfcl  18152  2ndfcl  18153  catcxpccl  18162  evlf2  18173  evlf1  18175  evlfcl  18177  hof1fval  18208  hof2fval  18210  hofcl  18214  ipoval  18485  letsr  18548  frmdplusg  18811  smndex1gbas  18859  smndex1gid  18861  smndex1igid  18863  eqgfval  19140  efglem  19680  efgval  19681  cnfldds  21354  cnfldfun  21356  cnfldfunALT  21357  cnflddsOLD  21367  cnfldfunOLD  21369  cnfldfunALTOLD  21370  xrsadd  21373  xrsmul  21374  xrsds  21397  pzriprnglem13  21481  pzriprnglem14  21482  znle  21524  pjfval  21694  psrplusg  21924  ltbval  22030  opsrle  22034  evlslem2  22066  evlsvvval  22080  evlssca  22081  mpfind  22102  psdmul  22141  evls1sca  22297  pf1ind  22329  mat1dimmul  22450  2ndcctbss  23429  txuni2  23539  txbas  23541  eltx  23542  txcnp  23594  txcnmpt  23598  txrest  23605  txlm  23622  tx1stc  23624  tx2ndc  23625  txkgen  23626  txflf  23980  cnextfval  24036  distgp  24073  indistgp  24074  ustfn  24176  ustn0  24195  ussid  24234  ressuss  24236  ishtpy  24948  isphtpc  24970  elovolmlem  25450  dyadmbl  25576  vitali  25589  mbfimaopnlem  25631  dvfval  25873  plyeq0lem  26187  taylfval  26337  ulmval  26360  dmarea  26938  dchrplusg  27229  madefi  27924  addsval  27973  mulsval  28120  zsex  28391  istrkg2ld  28547  tgjustc1  28562  tgjustc2  28563  iscgrg  28599  ishlg  28689  ishpg  28846  iscgra  28896  isinag  28925  isleag  28934  axlowdimlem15  29044  axlowdim  29049  isgrpoi  30589  sspval  30814  0ofval  30878  ajfval  30900  hvmulex  31102  padct  32811  gsumwrd2dccat  33159  inftmrel  33261  isinftm  33262  smatrcl  33961  tpr2rico  34077  faeval  34411  mbfmco2  34430  br2base  34434  sxbrsigalem0  34436  sxbrsigalem3  34437  dya2iocrfn  34444  dya2iocct  34445  dya2iocnrect  34446  dya2iocuni  34448  dya2iocucvr  34449  sxbrsigalem2  34451  eulerpartlemgs2  34545  ccatmulgnn0dir  34707  afsval  34836  cvmlift2lem9  35514  satfv0  35561  satf00  35577  prv1n  35634  mexval  35705  mdvval  35707  mpstval  35738  brimg  36138  brrestrict  36152  colinearex  36263  poimirlem4  37956  poimirlem28  37980  mblfinlem1  37989  heiborlem3  38145  rrnval  38159  ismrer1  38170  dfcnvrefrels2  38940  dfcnvrefrels3  38941  lcvfbr  39477  cmtfvalN  39667  cvrfval  39725  dvhvbase  41544  dvhfvadd  41548  dvhfvsca  41557  dibval  41599  dibfna  41611  dicval  41633  hdmap1fval  42253  ltex  42695  leex  42696  subex  42697  mzpincl  43177  pellexlem3  43274  pellexlem4  43275  pellexlem5  43276  aomclem6  43502  trclexi  44062  rtrclexi  44063  brtrclfv2  44169  mnringmulrcld  44670  hoiprodcl2  46998  hoicvrrex  46999  ovn0lem  47008  ovnhoilem1  47044  ovnlecvr2  47053  opnvonmbllem1  47075  opnvonmbllem2  47076  ovolval2lem  47086  ovolval2  47087  ovolval3  47090  ovolval4lem2  47093  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  smflimlem6  47219  gpgvtx  48516  gpgiedg  48517  sectfn  49501  nelsubc3  49543  cofidvala  49588  cofidval  49591  diag1f1lem  49778  fucoelvv  49792  fucofvalne  49797  functhinclem1  49916  functhinclem3  49918  functermc2  49981  idfudiag1bas  49996  idfudiag1  49997  prstchomval  50031  elpglem3  50185  pgindnf  50188  aacllem  50273