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 692	1 ⊢ (𝐴 × 𝐵) ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440   × cxp 5622

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 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-opab 5161  df-xp 5630  df-rel 5631

This theorem is referenced by:  oprabex  7920  oprabex3  7921  mpoexw  8022  naddcllem  8604  fnpm  8771  mapsnf1o2  8832  ixpsnf1o  8876  xpsnen  8989  endisj  8992  xpcomen  8996  xpassen  8999  xpmapenlem  9072  unxpdomlem3  9158  hartogslem1  9447  rankxpl  9787  rankfu  9789  rankmapu  9790  rankxplim  9791  rankxplim2  9792  rankxplim3  9793  rankxpsuc  9794  r0weon  9922  infxpenlem  9923  infxpenc2lem2  9930  dfac3  10031  dfac5lem2  10034  dfac5lem3  10035  dfac5lem4  10036  dfac5lem4OLD  10038  unctb  10114  axcc2lem  10346  axdc3lem  10360  axdc4lem  10365  enqex  10833  nqex  10834  nrex1  10975  enrex  10978  axcnex  11058  zexALT  12508  cnexALT  12899  mpoaddex  12901  addex  12902  mpomulex  12903  mulex  12904  ixxex  13272  shftfval  14993  climconst2  15471  cpnnen  16154  ruclem13  16167  cnso  16172  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdsle  17382  prdshom  17387  prdsco  17388  xrsle  17525  fnmrc  17530  mrcfval  17531  mreacs  17581  comfffval  17621  oppccofval  17639  sectfval  17675  brssc  17738  sscpwex  17739  isssc  17744  isfunc  17788  isfuncd  17789  idfu2nd  17801  idfu1st  17803  idfucl  17805  wunfunc  17825  fuccofval  17886  homafval  17953  homaf  17954  homaval  17955  coapm  17995  catccofval  18028  catcfuccl  18042  xpcval  18100  xpcbas  18101  xpchom  18103  xpccofval  18105  1stfval  18114  2ndfval  18117  1stfcl  18120  2ndfcl  18121  catcxpccl  18130  evlf2  18141  evlf1  18143  evlfcl  18145  hof1fval  18176  hof2fval  18178  hofcl  18182  ipoval  18453  letsr  18516  frmdplusg  18779  eqgfval  19105  efglem  19645  efgval  19646  cnfldds  21321  cnfldfun  21323  cnfldfunALT  21324  cnflddsOLD  21334  cnfldfunOLD  21336  cnfldfunALTOLD  21337  xrsadd  21340  xrsmul  21341  xrsds  21364  pzriprnglem13  21448  pzriprnglem14  21449  znle  21491  pjfval  21661  psrplusg  21892  ltbval  21998  opsrle  22002  evlslem2  22034  evlsvvval  22048  evlssca  22049  mpfind  22070  psdmul  22109  evls1sca  22267  pf1ind  22299  mat1dimmul  22420  2ndcctbss  23399  txuni2  23509  txbas  23511  eltx  23512  txcnp  23564  txcnmpt  23568  txrest  23575  txlm  23592  tx1stc  23594  tx2ndc  23595  txkgen  23596  txflf  23950  cnextfval  24006  distgp  24043  indistgp  24044  ustfn  24146  ustn0  24165  ussid  24204  ressuss  24206  ishtpy  24927  isphtpc  24949  elovolmlem  25431  dyadmbl  25557  vitali  25570  mbfimaopnlem  25612  dvfval  25854  plyeq0lem  26171  taylfval  26322  ulmval  26345  dmarea  26923  dchrplusg  27214  madefi  27909  addsval  27958  mulsval  28105  zsex  28376  tgjustc1  28547  tgjustc2  28548  iscgrg  28584  ishlg  28674  ishpg  28831  iscgra  28881  isinag  28910  isleag  28919  axlowdimlem15  29029  axlowdim  29034  isgrpoi  30573  sspval  30798  0ofval  30862  ajfval  30884  hvmulex  31086  gsumwrd2dccat  33160  inftmrel  33262  isinftm  33263  smatrcl  33953  tpr2rico  34069  faeval  34403  mbfmco2  34422  br2base  34426  sxbrsigalem0  34428  sxbrsigalem3  34429  dya2iocrfn  34436  dya2iocct  34437  dya2iocnrect  34438  dya2iocuni  34440  dya2iocucvr  34441  sxbrsigalem2  34443  eulerpartlemgs2  34537  ccatmulgnn0dir  34699  afsval  34828  cvmlift2lem9  35505  satfv0  35552  satf00  35568  prv1n  35625  mexval  35696  mdvval  35698  mpstval  35729  brimg  36129  brrestrict  36143  colinearex  36254  poimirlem4  37821  poimirlem28  37845  mblfinlem1  37854  heiborlem3  38010  rrnval  38024  ismrer1  38035  dfcnvrefrels2  38777  dfcnvrefrels3  38778  lcvfbr  39276  cmtfvalN  39466  cvrfval  39524  dvhvbase  41343  dvhfvadd  41347  dvhfvsca  41356  dibval  41398  dibfna  41410  dicval  41432  hdmap1fval  42052  ltex  42496  leex  42497  subex  42498  mzpincl  42972  pellexlem3  43069  pellexlem4  43070  pellexlem5  43071  aomclem6  43297  trclexi  43857  rtrclexi  43858  brtrclfv2  43964  mnringmulrcld  44465  hoiprodcl2  46795  hoicvrrex  46796  ovn0lem  46805  ovnhoilem1  46841  ovnlecvr2  46850  opnvonmbllem1  46872  opnvonmbllem2  46873  ovolval2lem  46883  ovolval2  46884  ovolval3  46887  ovolval4lem2  46890  ovolval5lem2  46893  ovnovollem1  46896  ovnovollem2  46897  smflimlem6  47016  gpgvtx  48285  gpgiedg  48286  sectfn  49270  nelsubc3  49312  cofidvala  49357  cofidval  49360  diag1f1lem  49547  fucoelvv  49561  fucofvalne  49566  functhinclem1  49685  functhinclem3  49687  functermc2  49750  idfudiag1bas  49765  idfudiag1  49766  prstchomval  49800  elpglem3  49954  pgindnf  49957  aacllem  50042