Theorem xpex 7693

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-opab 5158  df-xp 5629  df-rel 5630

This theorem is referenced by:  oprabex  7918  oprabex3  7919  mpoexw  8020  naddcllem  8601  fnpm  8768  mapsnf1o2  8828  ixpsnf1o  8872  xpsnen  8985  endisj  8988  xpcomen  8992  xpassen  8995  xpmapenlem  9068  unxpdomlem3  9157  hartogslem1  9453  rankxpl  9790  rankfu  9792  rankmapu  9793  rankxplim  9794  rankxplim2  9795  rankxplim3  9796  rankxpsuc  9797  r0weon  9925  infxpenlem  9926  infxpenc2lem2  9933  dfac3  10034  dfac5lem2  10037  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  unctb  10117  axcc2lem  10349  axdc3lem  10363  axdc4lem  10368  enqex  10835  nqex  10836  nrex1  10977  enrex  10980  axcnex  11060  zexALT  12509  cnexALT  12905  mpoaddex  12907  addex  12908  mpomulex  12909  mulex  12910  ixxex  13277  shftfval  14995  climconst2  15473  cpnnen  16156  ruclem13  16169  cnso  16174  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdsle  17384  prdshom  17389  prdsco  17390  xrsle  17526  fnmrc  17531  mrcfval  17532  mreacs  17582  comfffval  17622  oppccofval  17640  sectfval  17676  brssc  17739  sscpwex  17740  isssc  17745  isfunc  17789  isfuncd  17790  idfu2nd  17802  idfu1st  17804  idfucl  17806  wunfunc  17826  fuccofval  17887  homafval  17954  homaf  17955  homaval  17956  coapm  17996  catccofval  18029  catcfuccl  18043  xpcval  18101  xpcbas  18102  xpchom  18104  xpccofval  18106  1stfval  18115  2ndfval  18118  1stfcl  18121  2ndfcl  18122  catcxpccl  18131  evlf2  18142  evlf1  18144  evlfcl  18146  hof1fval  18177  hof2fval  18179  hofcl  18183  ipoval  18454  letsr  18517  frmdplusg  18746  eqgfval  19073  efglem  19613  efgval  19614  cnfldds  21291  cnfldfun  21293  cnfldfunALT  21294  cnflddsOLD  21304  cnfldfunOLD  21306  cnfldfunALTOLD  21307  xrsadd  21310  xrsmul  21311  xrsds  21334  pzriprnglem13  21418  pzriprnglem14  21419  znle  21461  pjfval  21631  psrplusg  21861  ltbval  21966  opsrle  21970  evlslem2  22002  evlssca  22012  mpfind  22030  psdmul  22069  evls1sca  22226  pf1ind  22258  mat1dimmul  22379  2ndcctbss  23358  txuni2  23468  txbas  23470  eltx  23471  txcnp  23523  txcnmpt  23527  txrest  23534  txlm  23551  tx1stc  23553  tx2ndc  23554  txkgen  23555  txflf  23909  cnextfval  23965  distgp  24002  indistgp  24003  ustfn  24105  ustn0  24124  ussid  24164  ressuss  24166  ishtpy  24887  isphtpc  24909  elovolmlem  25391  dyadmbl  25517  vitali  25530  mbfimaopnlem  25572  dvfval  25814  plyeq0lem  26131  taylfval  26282  ulmval  26305  dmarea  26883  dchrplusg  27174  madefi  27845  addsval  27892  mulsval  28035  zsex  28291  tgjustc1  28438  tgjustc2  28439  iscgrg  28475  ishlg  28565  ishpg  28722  iscgra  28772  isinag  28801  isleag  28810  axlowdimlem15  28919  axlowdim  28924  isgrpoi  30460  sspval  30685  0ofval  30749  ajfval  30771  hvmulex  30973  gsumwrd2dccat  33033  inftmrel  33132  isinftm  33133  smatrcl  33762  tpr2rico  33878  faeval  34212  mbfmco2  34232  br2base  34236  sxbrsigalem0  34238  sxbrsigalem3  34239  dya2iocrfn  34246  dya2iocct  34247  dya2iocnrect  34248  dya2iocuni  34250  dya2iocucvr  34251  sxbrsigalem2  34253  eulerpartlemgs2  34347  ccatmulgnn0dir  34509  afsval  34638  cvmlift2lem9  35283  satfv0  35330  satf00  35346  prv1n  35403  mexval  35474  mdvval  35476  mpstval  35507  brimg  35910  brrestrict  35922  colinearex  36033  poimirlem4  37603  poimirlem28  37627  mblfinlem1  37636  heiborlem3  37792  rrnval  37806  ismrer1  37817  dfcnvrefrels2  38504  dfcnvrefrels3  38505  lcvfbr  38998  cmtfvalN  39188  cvrfval  39246  dvhvbase  41066  dvhfvadd  41070  dvhfvsca  41079  dibval  41121  dibfna  41133  dicval  41155  hdmap1fval  41775  ltex  42218  leex  42219  subex  42220  evlsvvval  42536  mzpincl  42707  pellexlem3  42804  pellexlem4  42805  pellexlem5  42806  aomclem6  43032  trclexi  43593  rtrclexi  43594  brtrclfv2  43700  mnringmulrcld  44201  hoiprodcl2  46537  hoicvrrex  46538  ovn0lem  46547  ovnhoilem1  46583  ovnlecvr2  46592  opnvonmbllem1  46614  opnvonmbllem2  46615  ovolval2lem  46625  ovolval2  46626  ovolval3  46629  ovolval4lem2  46632  ovolval5lem2  46635  ovnovollem1  46638  ovnovollem2  46639  smflimlem6  46758  gpgvtx  48028  gpgiedg  48029  sectfn  49015  nelsubc3  49057  cofidvala  49102  cofidval  49105  diag1f1lem  49292  fucoelvv  49306  fucofvalne  49311  functhinclem1  49430  functhinclem3  49432  functermc2  49495  idfudiag1bas  49510  idfudiag1  49511  prstchomval  49545  elpglem3  49699  pgindnf  49702  aacllem  49787