Theorem xpex 7767

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  oprabex  7988  oprabex3  7989  mpoexw  8091  naddcllem  8688  fnpm  8857  mapsnf1o2  8925  ixpsnf1o  8969  xpsnen  9083  endisj  9086  xpcomen  9090  xpassen  9093  xpmapenlem  9166  unxpdomlem3  9252  hartogslem1  9539  rankxpl  9895  rankfu  9897  rankmapu  9898  rankxplim  9899  rankxplim2  9900  rankxplim3  9901  rankxpsuc  9902  r0weon  10094  infxpenlem  10095  infxpenc2lem2  10102  dfac3  10203  dfac5lem2  10206  dfac5lem3  10207  dfac5lem4  10208  unctb  10285  axcc2lem  10517  axdc3lem  10531  axdc4lem  10536  enqex  11010  nqex  11011  nrex1  11152  enrex  11155  axcnex  11235  zexALT  12716  cnexALT  13117  mpoaddex  13119  addex  13120  mpomulex  13121  mulex  13122  ixxex  13490  shftfval  15228  climconst2  15720  cpnnen  16402  ruclem13  16415  cnso  16420  prdsplusg  17634  prdsmulr  17635  prdsvsca  17636  prdsle  17638  prdshom  17643  prdsco  17644  xrsle  17781  fnmrc  17786  mrcfval  17787  mreacs  17837  comfffval  17877  oppccofval  17895  sectfval  17931  brssc  17994  sscpwex  17995  isssc  18000  isfunc  18044  isfuncd  18045  idfu2nd  18057  idfu1st  18059  idfucl  18061  wunfunc  18081  fuccofval  18142  homafval  18209  homaf  18210  homaval  18211  coapm  18251  catccofval  18284  catcfuccl  18298  xpcval  18356  xpcbas  18357  xpchom  18359  xpccofval  18361  1stfval  18370  2ndfval  18373  1stfcl  18376  2ndfcl  18377  catcxpccl  18386  evlf2  18397  evlf1  18399  evlfcl  18401  hof1fval  18432  hof2fval  18434  hofcl  18438  ipoval  18709  letsr  18772  frmdplusg  19055  smndex1gbas  19103  smndex1gid  19105  smndex1igid  19107  eqgfval  19393  efglem  19935  efgval  19936  cnfldds  21695  cnfldfun  21697  cnfldfunALT  21698  xrsadd  21701  xrsmul  21702  xrsds  21721  pzriprnglem13  21804  pzriprnglem14  21805  znle  21847  pjfval  22017  psrplusg  22250  ltbval  22357  opsrle  22361  evlslem2  22393  evlsvvval  22407  evlssca  22408  mpfind  22429  psdmul  22492  evls1sca  22646  pf1ind  22678  mat1dimmul  22796  2ndcctbss  23779  txuni2  23889  txbas  23891  eltx  23892  txcnp  23944  txcnmpt  23948  txrest  23955  txlm  23972  tx1stc  23974  tx2ndc  23975  txkgen  23976  txflf  24330  cnextfval  24386  distgp  24423  indistgp  24424  ustfn  24526  ustn0  24545  ussid  24584  ressuss  24586  ishtpy  25298  isphtpc  25320  elovolmlem  25800  dyadmbl  25926  vitali  25939  mbfimaopnlem  25981  dvfval  26222  plyeq0lem  26534  taylfval  26691  ulmval  26712  dmarea  27290  dchrplusg  27579  addsval  28353  mulsval  28500  zsex  28771  istrkg2ld  28927  tgjustc1  28942  tgjustc2  28943  iscgrg  28980  ishlg2  29070  ishlg  29073  ishpg  29242  iscgra  29321  isinag  29362  isleag  29371  axlowdimlem15  29539  axlowdim  29544  isgrpoi  31105  sspval  31330  0ofval  31394  ajfval  31416  hvmulex  31618  padct  33357  gsumwrd2dccat  33685  inftmrel  33787  isinftm  33788  smatrcl  34474  tpr2rico  34590  faeval  34925  mbfmco2  34943  br2base  34947  sxbrsigalem0  34949  sxbrsigalem3  34950  dya2iocrfn  34957  dya2iocct  34958  dya2iocnrect  34959  dya2iocuni  34961  dya2iocucvr  34962  sxbrsigalem2  34964  eulerpartlemgs2  35058  ccatmulgnn0dir  35220  afsval  35349  dfac15  35809  vonf1onprcf1ac  35963  cvmlift2lem9  36162  satfv0  36209  satf00  36225  prv1n  36282  mexval  36353  mdvval  36355  mpstval  36386  brimg  36791  brrestrict  36805  colinearex  36917  nmulprop  37031  poimirlem4  38635  poimirlem28  38659  mblfinlem1  38668  heiborlem3  38840  rrnval  38854  ismrer1  38865  dfcnvrefrels2  39633  dfcnvrefrels3  39634  lcvfbr  40170  cmtfvalN  40360  cvrfval  40418  dvhvbase  42237  dvhfvadd  42241  dvhfvsca  42250  dibval  42292  dibfna  42304  dicval  42326  hdmap1fval  42946  ltex  43389  leex  43390  subex  43391  mzpincl  43838  pellexlem3  43931  pellexlem4  43932  pellexlem5  43933  aomclem6  44154  trclexi  44713  rtrclexi  44714  brtrclfv2  44820  mnringmulrcld  45319  hoiprodcl2  47658  hoicvrrex  47659  ovn0lem  47668  ovnhoilem1  47704  ovnlecvr2  47713  opnvonmbllem1  47735  opnvonmbllem2  47736  ovolval2lem  47746  ovolval2  47747  ovolval3  47750  ovolval4lem2  47753  ovolval5lem2  47756  ovnovollem1  47759  ovnovollem2  47760  gpgvtx  49234  gpgiedg  49235  sectfn  50236  nelsubc3  50278  cofidvala  50325  cofidval  50328  diag1f1lem  50521  fucoelvv  50535  fucofvalne  50540  functhinclem1  50672  functhinclem3  50674  functermc2  50737  idfudiag1bas  50752  idfudiag1  50753  prstchomval  50790  parcatid2  50856  parcatid  50857  par2str  50862  elpglem3  50974  pgindnf  50977  aacllem  51107