Theorem xpex 7223

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

Syntax hints:   ∈ wcel 2166  Vcvv 3414   × cxp 5340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-opab 4936  df-xp 5348  df-rel 5349

This theorem is referenced by:  oprabex  7416  oprabex3  7417  fnpm  8130  mapsnf1o2  8172  ixpsnf1o  8215  xpsnen  8313  endisj  8316  xpcomen  8320  xpassen  8323  xpmapenlem  8396  mapunen  8398  unxpdomlem3  8435  hartogslem1  8716  rankxpl  9015  rankfu  9017  rankmapu  9018  rankxplim  9019  rankxplim2  9020  rankxplim3  9021  rankxpsuc  9022  r0weon  9148  infxpenlem  9149  infxpenc2lem2  9156  dfac3  9257  dfac5lem2  9260  dfac5lem3  9261  dfac5lem4  9262  cdafn  9306  unctb  9342  axcc2lem  9573  axdc3lem  9587  axdc4lem  9592  enqex  10059  nqex  10060  nrex1  10201  enrex  10204  axcnex  10284  zexALT  11723  cnexALT  12108  addex  12110  mulex  12111  ixxex  12474  shftfval  14187  climconst2  14656  cpnnen  15332  ruclem13  15345  cnso  15350  prdsval  16468  prdsplusg  16471  prdsmulr  16472  prdsvsca  16473  prdsle  16475  prdsds  16477  prdshom  16480  prdsco  16481  fnmrc  16620  mrcfval  16621  mreacs  16671  comfffval  16710  oppccofval  16728  sectfval  16763  brssc  16826  sscpwex  16827  isssc  16832  isfunc  16876  isfuncd  16877  idfu2nd  16889  idfu1st  16891  idfucl  16893  wunfunc  16911  fuccofval  16971  homafval  17031  homaf  17032  homaval  17033  coapm  17073  catccofval  17102  catcfuccl  17111  xpcval  17170  xpcbas  17171  xpchom  17173  xpccofval  17175  1stfval  17184  2ndfval  17187  1stfcl  17190  2ndfcl  17191  catcxpccl  17200  evlf2  17211  evlf1  17213  evlfcl  17215  hof1fval  17246  hof2fval  17248  hofcl  17252  ipoval  17507  letsr  17580  plusffval  17600  frmdplusg  17745  eqgfval  17993  efglem  18480  efgval  18481  scaffval  19237  psrplusg  19742  ltbval  19832  opsrle  19836  evlslem2  19872  evlssca  19882  mpfind  19896  evls1sca  20048  pf1ind  20079  cnfldds  20116  cnfldfun  20118  cnfldfunALT  20119  xrsadd  20123  xrsmul  20124  xrsle  20126  xrsds  20149  znle  20244  ipffval  20355  pjfval  20413  mat1dimmul  20650  2ndcctbss  21629  txuni2  21739  txbas  21741  eltx  21742  txcnp  21794  txcnmpt  21798  txrest  21805  txlm  21822  tx1stc  21824  tx2ndc  21825  txkgen  21826  txflf  22180  cnextfval  22236  distgp  22273  indistgp  22274  ustfn  22375  ustn0  22394  ussid  22434  ressuss  22437  ishtpy  23141  isphtpc  23163  elovolmlem  23640  dyadmbl  23766  vitali  23779  mbfimaopnlem  23821  dvfval  24060  plyeq0lem  24365  taylfval  24512  ulmval  24533  dmarea  25097  dchrplusg  25385  tgjustc1  25787  tgjustc2  25788  iscgrg  25824  ishlg  25914  ishpg  26068  iscgra  26118  isinag  26147  axlowdimlem15  26255  axlowdim  26260  isgrpoi  27908  sspval  28133  0ofval  28197  ajfval  28219  hvmulex  28423  inftmrel  30279  isinftm  30280  smatrcl  30407  tpr2rico  30503  faeval  30854  mbfmco2  30872  br2base  30876  sxbrsigalem0  30878  sxbrsigalem3  30879  dya2iocrfn  30886  dya2iocct  30887  dya2iocnrect  30888  dya2iocuni  30890  dya2iocucvr  30891  sxbrsigalem2  30893  eulerpartlemgs2  30987  ccatmulgnn0dir  31166  afsval  31298  cvmlift2lem9  31839  mexval  31945  mdvval  31947  mpstval  31978  brimg  32583  brrestrict  32595  colinearex  32706  cnfinltrel  33786  poimirlem4  33957  poimirlem28  33981  mblfinlem1  33990  heiborlem3  34154  rrnval  34168  ismrer1  34179  dfcnvrefrels2  34824  dfcnvrefrels3  34825  lcvfbr  35095  cmtfvalN  35285  cvrfval  35343  dvhvbase  37162  dvhfvadd  37166  dvhfvsca  37175  dibval  37217  dibfna  37229  dicval  37251  hdmap1fval  37871  mzpincl  38141  pellexlem3  38239  pellexlem4  38240  pellexlem5  38241  aomclem6  38472  trclexi  38768  rtrclexi  38769  brtrclfv2  38860  hoiprodcl2  41563  hoicvrrex  41564  ovn0lem  41573  ovnhoilem1  41609  ovnlecvr2  41618  opnvonmbllem1  41640  opnvonmbllem2  41641  ovolval2lem  41651  ovolval2  41652  ovolval3  41655  ovolval4lem2  41658  ovolval5lem2  41661  ovnovollem1  41664  ovnovollem2  41665  smflimlem6  41778  elpglem3  43354  aacllem  43443