Theorem xpex 7456

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-opab 5093  df-xp 5525  df-rel 5526

This theorem is referenced by:  oprabex  7659  oprabex3  7660  mpoexw  7759  fnpm  8397  mapsnf1o2  8441  ixpsnf1o  8485  xpsnen  8584  endisj  8587  xpcomen  8591  xpassen  8594  xpmapenlem  8668  mapunen  8670  unxpdomlem3  8708  hartogslem1  8990  rankxpl  9288  rankfu  9290  rankmapu  9291  rankxplim  9292  rankxplim2  9293  rankxplim3  9294  rankxpsuc  9295  r0weon  9423  infxpenlem  9424  infxpenc2lem2  9431  dfac3  9532  dfac5lem2  9535  dfac5lem3  9536  dfac5lem4  9537  unctb  9616  axcc2lem  9847  axdc3lem  9861  axdc4lem  9866  enqex  10333  nqex  10334  nrex1  10475  enrex  10478  axcnex  10558  zexALT  11989  cnexALT  12373  addex  12375  mulex  12376  ixxex  12737  shftfval  14421  climconst2  14897  cpnnen  15574  ruclem13  15587  cnso  15592  prdsval  16720  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdsle  16727  prdshom  16732  prdsco  16733  fnmrc  16870  mrcfval  16871  mreacs  16921  comfffval  16960  oppccofval  16978  sectfval  17013  brssc  17076  sscpwex  17077  isssc  17082  isfunc  17126  isfuncd  17127  idfu2nd  17139  idfu1st  17141  idfucl  17143  wunfunc  17161  fuccofval  17221  homafval  17281  homaf  17282  homaval  17283  coapm  17323  catccofval  17352  catcfuccl  17361  xpcval  17419  xpcbas  17420  xpchom  17422  xpccofval  17424  1stfval  17433  2ndfval  17436  1stfcl  17439  2ndfcl  17440  catcxpccl  17449  evlf2  17460  evlf1  17462  evlfcl  17464  hof1fval  17495  hof2fval  17497  hofcl  17501  ipoval  17756  letsr  17829  frmdplusg  18011  eqgfval  18320  efglem  18834  efgval  18835  cnfldds  20101  cnfldfun  20103  cnfldfunALT  20104  xrsadd  20108  xrsmul  20109  xrsle  20111  xrsds  20134  znle  20228  pjfval  20395  psrplusg  20619  ltbval  20711  opsrle  20715  evlslem2  20751  evlssca  20761  mpfind  20779  evls1sca  20947  pf1ind  20979  mat1dimmul  21081  2ndcctbss  22060  txuni2  22170  txbas  22172  eltx  22173  txcnp  22225  txcnmpt  22229  txrest  22236  txlm  22253  tx1stc  22255  tx2ndc  22256  txkgen  22257  txflf  22611  cnextfval  22667  distgp  22704  indistgp  22705  ustfn  22807  ustn0  22826  ussid  22866  ressuss  22869  ishtpy  23577  isphtpc  23599  elovolmlem  24078  dyadmbl  24204  vitali  24217  mbfimaopnlem  24259  dvfval  24500  plyeq0lem  24807  taylfval  24954  ulmval  24975  dmarea  25543  dchrplusg  25831  tgjustc1  26269  tgjustc2  26270  iscgrg  26306  ishlg  26396  ishpg  26553  iscgra  26603  isinag  26632  isleag  26641  axlowdimlem15  26750  axlowdim  26755  isgrpoi  28281  sspval  28506  0ofval  28570  ajfval  28592  hvmulex  28794  inftmrel  30859  isinftm  30860  smatrcl  31149  tpr2rico  31265  faeval  31615  mbfmco2  31633  br2base  31637  sxbrsigalem0  31639  sxbrsigalem3  31640  dya2iocrfn  31647  dya2iocct  31648  dya2iocnrect  31649  dya2iocuni  31651  dya2iocucvr  31652  sxbrsigalem2  31654  eulerpartlemgs2  31748  ccatmulgnn0dir  31922  afsval  32052  cvmlift2lem9  32671  satfv0  32718  satf00  32734  prv1n  32791  mexval  32862  mdvval  32864  mpstval  32895  brimg  33511  brrestrict  33523  colinearex  33634  poimirlem4  35061  poimirlem28  35085  mblfinlem1  35094  heiborlem3  35251  rrnval  35265  ismrer1  35276  dfcnvrefrels2  35926  dfcnvrefrels3  35927  lcvfbr  36316  cmtfvalN  36506  cvrfval  36564  dvhvbase  38383  dvhfvadd  38387  dvhfvsca  38396  dibval  38438  dibfna  38450  dicval  38472  hdmap1fval  39092  mzpincl  39675  pellexlem3  39772  pellexlem4  39773  pellexlem5  39774  aomclem6  40003  trclexi  40320  rtrclexi  40321  brtrclfv2  40428  mnringmulrcld  40936  hoiprodcl2  43194  hoicvrrex  43195  ovn0lem  43204  ovnhoilem1  43240  ovnlecvr2  43249  opnvonmbllem1  43271  opnvonmbllem2  43272  ovolval2lem  43282  ovolval2  43283  ovolval3  43286  ovolval4lem2  43289  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296  smflimlem6  43409  elpglem3  45242  aacllem  45329