Theorem xpex 7470

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

Syntax hints:   ∈ wcel 2110  Vcvv 3495   × cxp 5548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-opab 5122  df-xp 5556  df-rel 5557

This theorem is referenced by:  oprabex  7671  oprabex3  7672  mpoexw  7770  fnpm  8408  mapsnf1o2  8452  ixpsnf1o  8496  xpsnen  8595  endisj  8598  xpcomen  8602  xpassen  8605  xpmapenlem  8678  mapunen  8680  unxpdomlem3  8718  hartogslem1  9000  rankxpl  9298  rankfu  9300  rankmapu  9301  rankxplim  9302  rankxplim2  9303  rankxplim3  9304  rankxpsuc  9305  r0weon  9432  infxpenlem  9433  infxpenc2lem2  9440  dfac3  9541  dfac5lem2  9544  dfac5lem3  9545  dfac5lem4  9546  unctb  9621  axcc2lem  9852  axdc3lem  9866  axdc4lem  9871  enqex  10338  nqex  10339  nrex1  10480  enrex  10483  axcnex  10563  zexALT  11995  cnexALT  12379  addex  12381  mulex  12382  ixxex  12743  shftfval  14423  climconst2  14899  cpnnen  15576  ruclem13  15589  cnso  15594  prdsval  16722  prdsplusg  16725  prdsmulr  16726  prdsvsca  16727  prdsle  16729  prdsds  16731  prdshom  16734  prdsco  16735  fnmrc  16872  mrcfval  16873  mreacs  16923  comfffval  16962  oppccofval  16980  sectfval  17015  brssc  17078  sscpwex  17079  isssc  17084  isfunc  17128  isfuncd  17129  idfu2nd  17141  idfu1st  17143  idfucl  17145  wunfunc  17163  fuccofval  17223  homafval  17283  homaf  17284  homaval  17285  coapm  17325  catccofval  17354  catcfuccl  17363  xpcval  17421  xpcbas  17422  xpchom  17424  xpccofval  17426  1stfval  17435  2ndfval  17438  1stfcl  17441  2ndfcl  17442  catcxpccl  17451  evlf2  17462  evlf1  17464  evlfcl  17466  hof1fval  17497  hof2fval  17499  hofcl  17503  ipoval  17758  letsr  17831  frmdplusg  18013  eqgfval  18322  efglem  18836  efgval  18837  psrplusg  20155  ltbval  20246  opsrle  20250  evlslem2  20286  evlssca  20296  mpfind  20314  evls1sca  20480  pf1ind  20512  cnfldds  20549  cnfldfun  20551  cnfldfunALT  20552  xrsadd  20556  xrsmul  20557  xrsle  20559  xrsds  20582  znle  20677  pjfval  20844  mat1dimmul  21079  2ndcctbss  22057  txuni2  22167  txbas  22169  eltx  22170  txcnp  22222  txcnmpt  22226  txrest  22233  txlm  22250  tx1stc  22252  tx2ndc  22253  txkgen  22254  txflf  22608  cnextfval  22664  distgp  22701  indistgp  22702  ustfn  22804  ustn0  22823  ussid  22863  ressuss  22866  ishtpy  23570  isphtpc  23592  elovolmlem  24069  dyadmbl  24195  vitali  24208  mbfimaopnlem  24250  dvfval  24489  plyeq0lem  24794  taylfval  24941  ulmval  24962  dmarea  25529  dchrplusg  25817  tgjustc1  26255  tgjustc2  26256  iscgrg  26292  ishlg  26382  ishpg  26539  iscgra  26589  isinag  26618  isleag  26627  axlowdimlem15  26736  axlowdim  26741  isgrpoi  28269  sspval  28494  0ofval  28558  ajfval  28580  hvmulex  28782  inftmrel  30804  isinftm  30805  smatrcl  31056  tpr2rico  31150  faeval  31500  mbfmco2  31518  br2base  31522  sxbrsigalem0  31524  sxbrsigalem3  31525  dya2iocrfn  31532  dya2iocct  31533  dya2iocnrect  31534  dya2iocuni  31536  dya2iocucvr  31537  sxbrsigalem2  31539  eulerpartlemgs2  31633  ccatmulgnn0dir  31807  afsval  31937  cvmlift2lem9  32553  satfv0  32600  satf00  32616  prv1n  32673  mexval  32744  mdvval  32746  mpstval  32777  brimg  33393  brrestrict  33405  colinearex  33516  poimirlem4  34890  poimirlem28  34914  mblfinlem1  34923  heiborlem3  35085  rrnval  35099  ismrer1  35110  dfcnvrefrels2  35760  dfcnvrefrels3  35761  lcvfbr  36150  cmtfvalN  36340  cvrfval  36398  dvhvbase  38217  dvhfvadd  38221  dvhfvsca  38230  dibval  38272  dibfna  38284  dicval  38306  hdmap1fval  38926  mzpincl  39324  pellexlem3  39421  pellexlem4  39422  pellexlem5  39423  aomclem6  39652  trclexi  39973  rtrclexi  39974  brtrclfv2  40065  hoiprodcl2  42830  hoicvrrex  42831  ovn0lem  42840  ovnhoilem1  42876  ovnlecvr2  42885  opnvonmbllem1  42907  opnvonmbllem2  42908  ovolval2lem  42918  ovolval2  42919  ovolval3  42922  ovolval4lem2  42925  ovolval5lem2  42928  ovnovollem1  42931  ovnovollem2  42932  smflimlem6  43045  elpglem3  44808  aacllem  44895