Theorem xpex 7692

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437   × cxp 5617

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 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-opab 5156  df-xp 5625  df-rel 5626

This theorem is referenced by:  oprabex  7914  oprabex3  7915  mpoexw  8016  naddcllem  8597  fnpm  8764  mapsnf1o2  8824  ixpsnf1o  8868  xpsnen  8981  endisj  8984  xpcomen  8988  xpassen  8991  xpmapenlem  9064  unxpdomlem3  9149  hartogslem1  9435  rankxpl  9775  rankfu  9777  rankmapu  9778  rankxplim  9779  rankxplim2  9780  rankxplim3  9781  rankxpsuc  9782  r0weon  9910  infxpenlem  9911  infxpenc2lem2  9918  dfac3  10019  dfac5lem2  10022  dfac5lem3  10023  dfac5lem4  10024  dfac5lem4OLD  10026  unctb  10102  axcc2lem  10334  axdc3lem  10348  axdc4lem  10353  enqex  10820  nqex  10821  nrex1  10962  enrex  10965  axcnex  11045  zexALT  12495  cnexALT  12886  mpoaddex  12888  addex  12889  mpomulex  12890  mulex  12891  ixxex  13258  shftfval  14979  climconst2  15457  cpnnen  16140  ruclem13  16153  cnso  16158  prdsplusg  17364  prdsmulr  17365  prdsvsca  17366  prdsle  17368  prdshom  17373  prdsco  17374  xrsle  17510  fnmrc  17515  mrcfval  17516  mreacs  17566  comfffval  17606  oppccofval  17624  sectfval  17660  brssc  17723  sscpwex  17724  isssc  17729  isfunc  17773  isfuncd  17774  idfu2nd  17786  idfu1st  17788  idfucl  17790  wunfunc  17810  fuccofval  17871  homafval  17938  homaf  17939  homaval  17940  coapm  17980  catccofval  18013  catcfuccl  18027  xpcval  18085  xpcbas  18086  xpchom  18088  xpccofval  18090  1stfval  18099  2ndfval  18102  1stfcl  18105  2ndfcl  18106  catcxpccl  18115  evlf2  18126  evlf1  18128  evlfcl  18130  hof1fval  18161  hof2fval  18163  hofcl  18167  ipoval  18438  letsr  18501  frmdplusg  18764  eqgfval  19090  efglem  19630  efgval  19631  cnfldds  21305  cnfldfun  21307  cnfldfunALT  21308  cnflddsOLD  21318  cnfldfunOLD  21320  cnfldfunALTOLD  21321  xrsadd  21324  xrsmul  21325  xrsds  21348  pzriprnglem13  21432  pzriprnglem14  21433  znle  21475  pjfval  21645  psrplusg  21875  ltbval  21979  opsrle  21983  evlslem2  22015  evlssca  22025  mpfind  22043  psdmul  22082  evls1sca  22239  pf1ind  22271  mat1dimmul  22392  2ndcctbss  23371  txuni2  23481  txbas  23483  eltx  23484  txcnp  23536  txcnmpt  23540  txrest  23547  txlm  23564  tx1stc  23566  tx2ndc  23567  txkgen  23568  txflf  23922  cnextfval  23978  distgp  24015  indistgp  24016  ustfn  24118  ustn0  24137  ussid  24176  ressuss  24178  ishtpy  24899  isphtpc  24921  elovolmlem  25403  dyadmbl  25529  vitali  25542  mbfimaopnlem  25584  dvfval  25826  plyeq0lem  26143  taylfval  26294  ulmval  26317  dmarea  26895  dchrplusg  27186  madefi  27859  addsval  27906  mulsval  28049  zsex  28305  tgjustc1  28454  tgjustc2  28455  iscgrg  28491  ishlg  28581  ishpg  28738  iscgra  28788  isinag  28817  isleag  28826  axlowdimlem15  28936  axlowdim  28941  isgrpoi  30480  sspval  30705  0ofval  30769  ajfval  30791  hvmulex  30993  gsumwrd2dccat  33054  inftmrel  33156  isinftm  33157  smatrcl  33830  tpr2rico  33946  faeval  34280  mbfmco2  34299  br2base  34303  sxbrsigalem0  34305  sxbrsigalem3  34306  dya2iocrfn  34313  dya2iocct  34314  dya2iocnrect  34315  dya2iocuni  34317  dya2iocucvr  34318  sxbrsigalem2  34320  eulerpartlemgs2  34414  ccatmulgnn0dir  34576  afsval  34705  cvmlift2lem9  35376  satfv0  35423  satf00  35439  prv1n  35496  mexval  35567  mdvval  35569  mpstval  35600  brimg  36000  brrestrict  36014  colinearex  36125  poimirlem4  37684  poimirlem28  37708  mblfinlem1  37717  heiborlem3  37873  rrnval  37887  ismrer1  37898  dfcnvrefrels2  38640  dfcnvrefrels3  38641  lcvfbr  39139  cmtfvalN  39329  cvrfval  39387  dvhvbase  41206  dvhfvadd  41210  dvhfvsca  41219  dibval  41261  dibfna  41273  dicval  41295  hdmap1fval  41915  ltex  42363  leex  42364  subex  42365  evlsvvval  42681  mzpincl  42851  pellexlem3  42948  pellexlem4  42949  pellexlem5  42950  aomclem6  43176  trclexi  43737  rtrclexi  43738  brtrclfv2  43844  mnringmulrcld  44345  hoiprodcl2  46677  hoicvrrex  46678  ovn0lem  46687  ovnhoilem1  46723  ovnlecvr2  46732  opnvonmbllem1  46754  opnvonmbllem2  46755  ovolval2lem  46765  ovolval2  46766  ovolval3  46769  ovolval4lem2  46772  ovolval5lem2  46775  ovnovollem1  46778  ovnovollem2  46779  smflimlem6  46898  gpgvtx  48167  gpgiedg  48168  sectfn  49154  nelsubc3  49196  cofidvala  49241  cofidval  49244  diag1f1lem  49431  fucoelvv  49445  fucofvalne  49450  functhinclem1  49569  functhinclem3  49571  functermc2  49634  idfudiag1bas  49649  idfudiag1  49650  prstchomval  49684  elpglem3  49838  pgindnf  49841  aacllem  49926