Theorem xpex 7578

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

Syntax hints:   ∈ wcel 2112  Vcvv 3423   × cxp 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-opab 5133  df-xp 5585  df-rel 5586

This theorem is referenced by:  oprabex  7789  oprabex3  7790  mpoexw  7889  fnpm  8558  mapsnf1o2  8617  ixpsnf1o  8661  xpsnen  8773  endisj  8776  xpcomen  8780  xpassen  8783  xpmapenlem  8857  unxpdomlem3  8932  hartogslem1  9206  rankxpl  9539  rankfu  9541  rankmapu  9542  rankxplim  9543  rankxplim2  9544  rankxplim3  9545  rankxpsuc  9546  r0weon  9674  infxpenlem  9675  infxpenc2lem2  9682  dfac3  9783  dfac5lem2  9786  dfac5lem3  9787  dfac5lem4  9788  unctb  9867  axcc2lem  10098  axdc3lem  10112  axdc4lem  10117  enqex  10584  nqex  10585  nrex1  10726  enrex  10729  axcnex  10809  zexALT  12244  cnexALT  12630  addex  12632  mulex  12633  ixxex  12994  shftfval  14684  climconst2  15160  cpnnen  15841  ruclem13  15854  cnso  15859  prdsplusg  17061  prdsmulr  17062  prdsvsca  17063  prdsle  17065  prdshom  17070  prdsco  17071  fnmrc  17208  mrcfval  17209  mreacs  17259  comfffval  17299  oppccofval  17318  sectfval  17355  brssc  17418  sscpwex  17419  isssc  17424  isfunc  17470  isfuncd  17471  idfu2nd  17483  idfu1st  17485  idfucl  17487  wunfunc  17505  wunfuncOLD  17506  fuccofval  17567  homafval  17635  homaf  17636  homaval  17637  coapm  17677  catccofval  17710  catcfuccl  17725  catcfucclOLD  17726  xpcval  17785  xpcbas  17786  xpchom  17788  xpccofval  17790  1stfval  17799  2ndfval  17802  1stfcl  17805  2ndfcl  17806  catcxpccl  17815  catcxpcclOLD  17816  evlf2  17827  evlf1  17829  evlfcl  17831  hof1fval  17862  hof2fval  17864  hofcl  17868  ipoval  18138  letsr  18201  frmdplusg  18383  eqgfval  18694  efglem  19212  efgval  19213  cnfldds  20495  cnfldfun  20497  cnfldfunALT  20498  xrsadd  20502  xrsmul  20503  xrsle  20505  xrsds  20528  znle  20627  pjfval  20798  psrplusg  21035  ltbval  21129  opsrle  21133  evlslem2  21174  evlssca  21184  mpfind  21202  evls1sca  21374  pf1ind  21406  mat1dimmul  21508  2ndcctbss  22489  txuni2  22599  txbas  22601  eltx  22602  txcnp  22654  txcnmpt  22658  txrest  22665  txlm  22682  tx1stc  22684  tx2ndc  22685  txkgen  22686  txflf  23040  cnextfval  23096  distgp  23133  indistgp  23134  ustfn  23236  ustn0  23255  ussid  23295  ressuss  23297  ishtpy  24016  isphtpc  24038  elovolmlem  24518  dyadmbl  24644  vitali  24657  mbfimaopnlem  24699  dvfval  24941  plyeq0lem  25251  taylfval  25398  ulmval  25419  dmarea  25987  dchrplusg  26275  tgjustc1  26715  tgjustc2  26716  iscgrg  26752  ishlg  26842  ishpg  26999  iscgra  27049  isinag  27078  isleag  27087  axlowdimlem15  27202  axlowdim  27207  isgrpoi  28736  sspval  28961  0ofval  29025  ajfval  29047  hvmulex  29249  inftmrel  31311  isinftm  31312  smatrcl  31623  tpr2rico  31739  faeval  32089  mbfmco2  32107  br2base  32111  sxbrsigalem0  32113  sxbrsigalem3  32114  dya2iocrfn  32121  dya2iocct  32122  dya2iocnrect  32123  dya2iocuni  32125  dya2iocucvr  32126  sxbrsigalem2  32128  eulerpartlemgs2  32222  ccatmulgnn0dir  32396  afsval  32526  cvmlift2lem9  33148  satfv0  33195  satf00  33211  prv1n  33268  mexval  33339  mdvval  33341  mpstval  33372  naddcllem  33733  addsval  34028  brimg  34141  brrestrict  34153  colinearex  34264  poimirlem4  35687  poimirlem28  35711  mblfinlem1  35720  heiborlem3  35877  rrnval  35891  ismrer1  35902  dfcnvrefrels2  36550  dfcnvrefrels3  36551  lcvfbr  36940  cmtfvalN  37130  cvrfval  37188  dvhvbase  39007  dvhfvadd  39011  dvhfvsca  39020  dibval  39062  dibfna  39074  dicval  39096  hdmap1fval  39716  evlsbagval  40170  mzpincl  40444  pellexlem3  40541  pellexlem4  40542  pellexlem5  40543  aomclem6  40772  trclexi  41089  rtrclexi  41090  brtrclfv2  41197  mnringmulrcld  41708  hoiprodcl2  43956  hoicvrrex  43957  ovn0lem  43966  ovnhoilem1  44002  ovnlecvr2  44011  opnvonmbllem1  44033  opnvonmbllem2  44034  ovolval2lem  44044  ovolval2  44045  ovolval3  44048  ovolval4lem2  44051  ovolval5lem2  44054  ovnovollem1  44057  ovnovollem2  44058  smflimlem6  44171  functhinclem1  46183  functhinclem3  46185  prstchomval  46214  elpglem3  46277  aacllem  46364