Theorem xpex 7755

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

Syntax hints:   ∈ wcel 2107  Vcvv 3463   × cxp 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-opab 5186  df-xp 5671  df-rel 5672

This theorem is referenced by:  oprabex  7983  oprabex3  7984  mpoexw  8085  naddcllem  8696  fnpm  8856  mapsnf1o2  8916  ixpsnf1o  8960  xpsnen  9077  endisj  9080  xpcomen  9085  xpassen  9088  xpmapenlem  9166  unxpdomlem3  9270  hartogslem1  9564  rankxpl  9897  rankfu  9899  rankmapu  9900  rankxplim  9901  rankxplim2  9902  rankxplim3  9903  rankxpsuc  9904  r0weon  10034  infxpenlem  10035  infxpenc2lem2  10042  dfac3  10143  dfac5lem2  10146  dfac5lem3  10147  dfac5lem4  10148  dfac5lem4OLD  10150  unctb  10226  axcc2lem  10458  axdc3lem  10472  axdc4lem  10477  enqex  10944  nqex  10945  nrex1  11086  enrex  11089  axcnex  11169  zexALT  12616  cnexALT  13010  mpoaddex  13012  addex  13013  mpomulex  13014  mulex  13015  ixxex  13380  shftfval  15091  climconst2  15566  cpnnen  16247  ruclem13  16260  cnso  16265  prdsplusg  17474  prdsmulr  17475  prdsvsca  17476  prdsle  17478  prdshom  17483  prdsco  17484  fnmrc  17621  mrcfval  17622  mreacs  17672  comfffval  17712  oppccofval  17730  sectfval  17766  brssc  17829  sscpwex  17830  isssc  17835  isfunc  17880  isfuncd  17881  idfu2nd  17893  idfu1st  17895  idfucl  17897  wunfunc  17917  fuccofval  17978  homafval  18045  homaf  18046  homaval  18047  coapm  18087  catccofval  18120  catcfuccl  18134  xpcval  18192  xpcbas  18193  xpchom  18195  xpccofval  18197  1stfval  18206  2ndfval  18209  1stfcl  18212  2ndfcl  18213  catcxpccl  18222  evlf2  18233  evlf1  18235  evlfcl  18237  hof1fval  18268  hof2fval  18270  hofcl  18274  ipoval  18544  letsr  18607  frmdplusg  18836  eqgfval  19163  efglem  19702  efgval  19703  cnfldds  21338  cnfldfun  21340  cnfldfunALT  21341  cnflddsOLD  21351  cnfldfunOLD  21353  cnfldfunALTOLD  21354  cnfldfunALTOLDOLD  21355  xrsadd  21359  xrsmul  21360  xrsle  21362  xrsds  21389  pzriprnglem13  21466  pzriprnglem14  21467  znle  21509  pjfval  21680  psrplusg  21910  ltbval  22015  opsrle  22019  evlslem2  22051  evlssca  22061  mpfind  22079  psdmul  22118  evls1sca  22275  pf1ind  22307  mat1dimmul  22430  2ndcctbss  23409  txuni2  23519  txbas  23521  eltx  23522  txcnp  23574  txcnmpt  23578  txrest  23585  txlm  23602  tx1stc  23604  tx2ndc  23605  txkgen  23606  txflf  23960  cnextfval  24016  distgp  24053  indistgp  24054  ustfn  24156  ustn0  24175  ussid  24215  ressuss  24217  ishtpy  24940  isphtpc  24962  elovolmlem  25445  dyadmbl  25571  vitali  25584  mbfimaopnlem  25626  dvfval  25868  plyeq0lem  26185  taylfval  26336  ulmval  26359  dmarea  26936  dchrplusg  27227  madefi  27886  addsval  27931  mulsval  28071  zsex  28302  tgjustc1  28419  tgjustc2  28420  iscgrg  28456  ishlg  28546  ishpg  28703  iscgra  28753  isinag  28782  isleag  28791  axlowdimlem15  28901  axlowdim  28906  isgrpoi  30445  sspval  30670  0ofval  30734  ajfval  30756  hvmulex  30958  gsumwrd2dccat  33009  inftmrel  33126  isinftm  33127  smatrcl  33754  tpr2rico  33870  faeval  34206  mbfmco2  34226  br2base  34230  sxbrsigalem0  34232  sxbrsigalem3  34233  dya2iocrfn  34240  dya2iocct  34241  dya2iocnrect  34242  dya2iocuni  34244  dya2iocucvr  34245  sxbrsigalem2  34247  eulerpartlemgs2  34341  ccatmulgnn0dir  34516  afsval  34645  cvmlift2lem9  35275  satfv0  35322  satf00  35338  prv1n  35395  mexval  35466  mdvval  35468  mpstval  35499  brimg  35897  brrestrict  35909  colinearex  36020  poimirlem4  37590  poimirlem28  37614  mblfinlem1  37623  heiborlem3  37779  rrnval  37793  ismrer1  37804  dfcnvrefrels2  38488  dfcnvrefrels3  38489  lcvfbr  38980  cmtfvalN  39170  cvrfval  39228  dvhvbase  41048  dvhfvadd  41052  dvhfvsca  41061  dibval  41103  dibfna  41115  dicval  41137  hdmap1fval  41757  ltex  42244  leex  42245  subex  42246  evlsvvval  42536  mzpincl  42708  pellexlem3  42805  pellexlem4  42806  pellexlem5  42807  aomclem6  43034  trclexi  43595  rtrclexi  43596  brtrclfv2  43702  mnringmulrcld  44204  hoiprodcl2  46527  hoicvrrex  46528  ovn0lem  46537  ovnhoilem1  46573  ovnlecvr2  46582  opnvonmbllem1  46604  opnvonmbllem2  46605  ovolval2lem  46615  ovolval2  46616  ovolval3  46619  ovolval4lem2  46622  ovolval5lem2  46625  ovnovollem1  46628  ovnovollem2  46629  smflimlem6  46748  gpgvtx  47960  gpgiedg  47961  diag1f1lem  48977  fucoelvv  48991  fucofvalne  48996  functhinclem1  49071  functhinclem3  49073  functermc2  49122  idfudiag1bas  49135  idfudiag1  49136  prstchomval  49164  elpglem3  49240  pgindnf  49243  aacllem  49328