Theorem xpex 7732

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  oprabex  7958  oprabex3  7959  mpoexw  8060  naddcllem  8643  fnpm  8810  mapsnf1o2  8870  ixpsnf1o  8914  xpsnen  9029  endisj  9032  xpcomen  9037  xpassen  9040  xpmapenlem  9114  unxpdomlem3  9206  hartogslem1  9502  rankxpl  9835  rankfu  9837  rankmapu  9838  rankxplim  9839  rankxplim2  9840  rankxplim3  9841  rankxpsuc  9842  r0weon  9972  infxpenlem  9973  infxpenc2lem2  9980  dfac3  10081  dfac5lem2  10084  dfac5lem3  10085  dfac5lem4  10086  dfac5lem4OLD  10088  unctb  10164  axcc2lem  10396  axdc3lem  10410  axdc4lem  10415  enqex  10882  nqex  10883  nrex1  11024  enrex  11027  axcnex  11107  zexALT  12556  cnexALT  12952  mpoaddex  12954  addex  12955  mpomulex  12956  mulex  12957  ixxex  13324  shftfval  15043  climconst2  15521  cpnnen  16204  ruclem13  16217  cnso  16222  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdsle  17432  prdshom  17437  prdsco  17438  fnmrc  17575  mrcfval  17576  mreacs  17626  comfffval  17666  oppccofval  17684  sectfval  17720  brssc  17783  sscpwex  17784  isssc  17789  isfunc  17833  isfuncd  17834  idfu2nd  17846  idfu1st  17848  idfucl  17850  wunfunc  17870  fuccofval  17931  homafval  17998  homaf  17999  homaval  18000  coapm  18040  catccofval  18073  catcfuccl  18087  xpcval  18145  xpcbas  18146  xpchom  18148  xpccofval  18150  1stfval  18159  2ndfval  18162  1stfcl  18165  2ndfcl  18166  catcxpccl  18175  evlf2  18186  evlf1  18188  evlfcl  18190  hof1fval  18221  hof2fval  18223  hofcl  18227  ipoval  18496  letsr  18559  frmdplusg  18788  eqgfval  19115  efglem  19653  efgval  19654  cnfldds  21283  cnfldfun  21285  cnfldfunALT  21286  cnflddsOLD  21296  cnfldfunOLD  21298  cnfldfunALTOLD  21299  xrsadd  21303  xrsmul  21304  xrsle  21306  xrsds  21333  pzriprnglem13  21410  pzriprnglem14  21411  znle  21453  pjfval  21622  psrplusg  21852  ltbval  21957  opsrle  21961  evlslem2  21993  evlssca  22003  mpfind  22021  psdmul  22060  evls1sca  22217  pf1ind  22249  mat1dimmul  22370  2ndcctbss  23349  txuni2  23459  txbas  23461  eltx  23462  txcnp  23514  txcnmpt  23518  txrest  23525  txlm  23542  tx1stc  23544  tx2ndc  23545  txkgen  23546  txflf  23900  cnextfval  23956  distgp  23993  indistgp  23994  ustfn  24096  ustn0  24115  ussid  24155  ressuss  24157  ishtpy  24878  isphtpc  24900  elovolmlem  25382  dyadmbl  25508  vitali  25521  mbfimaopnlem  25563  dvfval  25805  plyeq0lem  26122  taylfval  26273  ulmval  26296  dmarea  26874  dchrplusg  27165  madefi  27831  addsval  27876  mulsval  28019  zsex  28275  tgjustc1  28409  tgjustc2  28410  iscgrg  28446  ishlg  28536  ishpg  28693  iscgra  28743  isinag  28772  isleag  28781  axlowdimlem15  28890  axlowdim  28895  isgrpoi  30434  sspval  30659  0ofval  30723  ajfval  30745  hvmulex  30947  gsumwrd2dccat  33014  inftmrel  33141  isinftm  33142  smatrcl  33793  tpr2rico  33909  faeval  34243  mbfmco2  34263  br2base  34267  sxbrsigalem0  34269  sxbrsigalem3  34270  dya2iocrfn  34277  dya2iocct  34278  dya2iocnrect  34279  dya2iocuni  34281  dya2iocucvr  34282  sxbrsigalem2  34284  eulerpartlemgs2  34378  ccatmulgnn0dir  34540  afsval  34669  cvmlift2lem9  35305  satfv0  35352  satf00  35368  prv1n  35425  mexval  35496  mdvval  35498  mpstval  35529  brimg  35932  brrestrict  35944  colinearex  36055  poimirlem4  37625  poimirlem28  37649  mblfinlem1  37658  heiborlem3  37814  rrnval  37828  ismrer1  37839  dfcnvrefrels2  38526  dfcnvrefrels3  38527  lcvfbr  39020  cmtfvalN  39210  cvrfval  39268  dvhvbase  41088  dvhfvadd  41092  dvhfvsca  41101  dibval  41143  dibfna  41155  dicval  41177  hdmap1fval  41797  ltex  42240  leex  42241  subex  42242  evlsvvval  42558  mzpincl  42729  pellexlem3  42826  pellexlem4  42827  pellexlem5  42828  aomclem6  43055  trclexi  43616  rtrclexi  43617  brtrclfv2  43723  mnringmulrcld  44224  hoiprodcl2  46560  hoicvrrex  46561  ovn0lem  46570  ovnhoilem1  46606  ovnlecvr2  46615  opnvonmbllem1  46637  opnvonmbllem2  46638  ovolval2lem  46648  ovolval2  46649  ovolval3  46652  ovolval4lem2  46655  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  smflimlem6  46781  gpgvtx  48038  gpgiedg  48039  sectfn  49022  nelsubc3  49064  cofidvala  49109  cofidval  49112  diag1f1lem  49299  fucoelvv  49313  fucofvalne  49318  functhinclem1  49437  functhinclem3  49439  functermc2  49502  idfudiag1bas  49517  idfudiag1  49518  prstchomval  49552  elpglem3  49706  pgindnf  49709  aacllem  49794