Theorem xpex 7494

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

Syntax hints:   ∈ wcel 2114  Vcvv 3398   × cxp 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-opab 5093  df-xp 5531  df-rel 5532

This theorem is referenced by:  oprabex  7702  oprabex3  7703  mpoexw  7802  fnpm  8445  mapsnf1o2  8504  ixpsnf1o  8548  xpsnen  8650  endisj  8653  xpcomen  8657  xpassen  8660  xpmapenlem  8734  unxpdomlem3  8803  hartogslem1  9079  rankxpl  9377  rankfu  9379  rankmapu  9380  rankxplim  9381  rankxplim2  9382  rankxplim3  9383  rankxpsuc  9384  r0weon  9512  infxpenlem  9513  infxpenc2lem2  9520  dfac3  9621  dfac5lem2  9624  dfac5lem3  9625  dfac5lem4  9626  unctb  9705  axcc2lem  9936  axdc3lem  9950  axdc4lem  9955  enqex  10422  nqex  10423  nrex1  10564  enrex  10567  axcnex  10647  zexALT  12082  cnexALT  12468  addex  12470  mulex  12471  ixxex  12832  shftfval  14519  climconst2  14995  cpnnen  15674  ruclem13  15687  cnso  15692  prdsval  16831  prdsplusg  16834  prdsmulr  16835  prdsvsca  16836  prdsle  16838  prdshom  16843  prdsco  16844  fnmrc  16981  mrcfval  16982  mreacs  17032  comfffval  17072  oppccofval  17090  sectfval  17126  brssc  17189  sscpwex  17190  isssc  17195  isfunc  17239  isfuncd  17240  idfu2nd  17252  idfu1st  17254  idfucl  17256  wunfunc  17274  fuccofval  17334  homafval  17401  homaf  17402  homaval  17403  coapm  17443  catccofval  17476  catcfuccl  17485  xpcval  17543  xpcbas  17544  xpchom  17546  xpccofval  17548  1stfval  17557  2ndfval  17560  1stfcl  17563  2ndfcl  17564  catcxpccl  17573  evlf2  17584  evlf1  17586  evlfcl  17588  hof1fval  17619  hof2fval  17621  hofcl  17625  ipoval  17880  letsr  17953  frmdplusg  18135  eqgfval  18446  efglem  18960  efgval  18961  cnfldds  20227  cnfldfun  20229  cnfldfunALT  20230  xrsadd  20234  xrsmul  20235  xrsle  20237  xrsds  20260  znle  20355  pjfval  20522  psrplusg  20760  ltbval  20854  opsrle  20858  evlslem2  20893  evlssca  20903  mpfind  20921  evls1sca  21093  pf1ind  21125  mat1dimmul  21227  2ndcctbss  22206  txuni2  22316  txbas  22318  eltx  22319  txcnp  22371  txcnmpt  22375  txrest  22382  txlm  22399  tx1stc  22401  tx2ndc  22402  txkgen  22403  txflf  22757  cnextfval  22813  distgp  22850  indistgp  22851  ustfn  22953  ustn0  22972  ussid  23012  ressuss  23015  ishtpy  23724  isphtpc  23746  elovolmlem  24226  dyadmbl  24352  vitali  24365  mbfimaopnlem  24407  dvfval  24649  plyeq0lem  24959  taylfval  25106  ulmval  25127  dmarea  25695  dchrplusg  25983  tgjustc1  26421  tgjustc2  26422  iscgrg  26458  ishlg  26548  ishpg  26705  iscgra  26755  isinag  26784  isleag  26793  axlowdimlem15  26902  axlowdim  26907  isgrpoi  28433  sspval  28658  0ofval  28722  ajfval  28744  hvmulex  28946  inftmrel  31011  isinftm  31012  smatrcl  31318  tpr2rico  31434  faeval  31784  mbfmco2  31802  br2base  31806  sxbrsigalem0  31808  sxbrsigalem3  31809  dya2iocrfn  31816  dya2iocct  31817  dya2iocnrect  31818  dya2iocuni  31820  dya2iocucvr  31821  sxbrsigalem2  31823  eulerpartlemgs2  31917  ccatmulgnn0dir  32091  afsval  32221  cvmlift2lem9  32844  satfv0  32891  satf00  32907  prv1n  32964  mexval  33035  mdvval  33037  mpstval  33068  naddcllem  33472  addsov  33764  brimg  33877  brrestrict  33889  colinearex  34000  poimirlem4  35404  poimirlem28  35428  mblfinlem1  35437  heiborlem3  35594  rrnval  35608  ismrer1  35619  dfcnvrefrels2  36267  dfcnvrefrels3  36268  lcvfbr  36657  cmtfvalN  36847  cvrfval  36905  dvhvbase  38724  dvhfvadd  38728  dvhfvsca  38737  dibval  38779  dibfna  38791  dicval  38813  hdmap1fval  39433  evlsbagval  39854  mzpincl  40128  pellexlem3  40225  pellexlem4  40226  pellexlem5  40227  aomclem6  40456  trclexi  40773  rtrclexi  40774  brtrclfv2  40881  mnringmulrcld  41388  hoiprodcl2  43635  hoicvrrex  43636  ovn0lem  43645  ovnhoilem1  43681  ovnlecvr2  43690  opnvonmbllem1  43712  opnvonmbllem2  43713  ovolval2lem  43723  ovolval2  43724  ovolval3  43727  ovolval4lem2  43730  ovolval5lem2  43733  ovnovollem1  43736  ovnovollem2  43737  smflimlem6  43850  prstchomval  45812  elpglem3  45871  aacllem  45958