Theorem xpex 6860

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-opab 4644  df-xp 5044  df-rel 5045

This theorem is referenced by:  oprabex  7047  oprabex3  7048  fnpm  7752  mapsnf1o2  7791  ixpsnf1o  7834  xpsnen  7929  endisj  7932  xpcomen  7936  xpassen  7939  xpmapenlem  8012  mapunen  8014  unxpdomlem3  8051  hartogslem1  8330  rankxpl  8621  rankfu  8623  rankmapu  8624  rankxplim  8625  rankxplim2  8626  rankxplim3  8627  rankxpsuc  8628  r0weon  8718  infxpenlem  8719  infxpenc2lem2  8726  dfac3  8827  dfac5lem2  8830  dfac5lem3  8831  dfac5lem4  8832  cdafn  8874  unctb  8910  axcc2lem  9141  axdc3lem  9155  axdc4lem  9160  enqex  9623  nqex  9624  enrex  9767  axcnex  9847  zexALT  11273  cnexALT  11704  addex  11706  mulex  11707  ixxex  12057  shftfval  13658  climconst2  14127  cpnnen  14797  ruclem13  14810  cnso  14815  prdsval  15938  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdsle  15945  prdsds  15947  prdshom  15950  prdsco  15951  fnmrc  16090  mrcfval  16091  mreacs  16142  comfffval  16181  oppccofval  16199  sectfval  16234  brssc  16297  sscpwex  16298  isssc  16303  isfunc  16347  isfuncd  16348  idfu2nd  16360  idfu1st  16362  idfucl  16364  wunfunc  16382  fuccofval  16442  homafval  16502  homaf  16503  homaval  16504  coapm  16544  catccofval  16573  catcfuccl  16582  xpcval  16640  xpcbas  16641  xpchom  16643  xpccofval  16645  1stfval  16654  2ndfval  16657  1stfcl  16660  2ndfcl  16661  catcxpccl  16670  evlf2  16681  evlf1  16683  evlfcl  16685  hof1fval  16716  hof2fval  16718  hofcl  16722  ipoval  16977  letsr  17050  plusffval  17070  frmdplusg  17214  eqgfval  17465  efglem  17952  efgval  17953  scaffval  18704  psrplusg  19202  ltbval  19292  opsrle  19296  evlslem2  19333  evlssca  19343  mpfind  19357  evls1sca  19509  pf1ind  19540  cnfldds  19577  xrsadd  19582  xrsmul  19583  xrsle  19585  xrsds  19608  znle  19703  ipffval  19812  pjfval  19869  mat1dimmul  20101  2ndcctbss  21068  txuni2  21178  txbas  21180  eltx  21181  txcnp  21233  txcnmpt  21237  txrest  21244  txlm  21261  tx1stc  21263  tx2ndc  21264  txkgen  21265  txflf  21620  cnextfval  21676  distgp  21713  indistgp  21714  ustfn  21815  ustn0  21834  ussid  21874  ressuss  21877  ishtpy  22579  isphtpc  22601  elovolm  23050  elovolmr  23051  ovolmge0  23052  ovolgelb  23055  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovolshftlem2  23085  ovolicc2  23097  ioombl1  23137  dyadmbl  23174  vitali  23188  mbfimaopnlem  23228  dvfval  23467  plyeq0lem  23770  taylfval  23917  ulmval  23938  dmarea  24484  dchrplusg  24772  iscgrg  25207  ishlg  25297  ishpg  25451  iscgra  25501  isinag  25529  axlowdimlem15  25636  axlowdim  25641  iseupa  26492  isgrpoi  26736  sspval  26962  0ofval  27026  ajfval  27048  hvmulex  27252  inftmrel  29065  isinftm  29066  smatrcl  29190  tpr2rico  29286  faeval  29636  mbfmco2  29654  br2base  29658  sxbrsigalem0  29660  sxbrsigalem3  29661  dya2iocrfn  29668  dya2iocct  29669  dya2iocnrect  29670  dya2iocuni  29672  dya2iocucvr  29673  sxbrsigalem2  29675  eulerpartlemgs2  29769  ccatmulgnn0dir  29945  afsval  30002  cvmlift2lem9  30547  mexval  30653  mdvval  30655  mpstval  30686  brimg  31214  brrestrict  31226  colinearex  31337  poimirlem4  32583  poimirlem28  32607  mblfinlem1  32616  heiborlem3  32782  rrnval  32796  ismrer1  32807  lcvfbr  33325  cmtfvalN  33515  cvrfval  33573  dvhvbase  35394  dvhfvadd  35398  dvhfvsca  35407  dibval  35449  dibfna  35461  dicval  35483  hdmap1fval  36104  mzpincl  36315  pellexlem3  36413  pellexlem4  36414  pellexlem5  36415  aomclem6  36647  trclexi  36946  rtrclexi  36947  brtrclfv2  37038  hoiprodcl2  39445  hoicvrrex  39446  ovn0lem  39455  ovnhoilem1  39491  ovnlecvr2  39500  opnvonmbllem1  39522  opnvonmbllem2  39523  ovolval2lem  39533  ovolval2  39534  ovolval3  39537  ovolval4lem2  39540  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  smflimlem6  39662  elpglem3  42255  aacllem  42356