Theorem xpex 7756

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  oprabex  7977  oprabex3  7978  mpoexw  8080  naddcllem  8669  fnpm  8838  mapsnf1o2  8906  ixpsnf1o  8950  xpsnen  9064  endisj  9067  xpcomen  9071  xpassen  9074  xpmapenlem  9147  unxpdomlem3  9233  hartogslem1  9520  rankxpl  9873  rankfu  9875  rankmapu  9876  rankxplim  9877  rankxplim2  9878  rankxplim3  9879  rankxpsuc  9880  r0weon  10072  infxpenlem  10073  infxpenc2lem2  10080  dfac3  10181  dfac5lem2  10184  dfac5lem3  10185  dfac5lem4  10186  unctb  10263  axcc2lem  10495  axdc3lem  10509  axdc4lem  10514  enqex  10988  nqex  10989  nrex1  11130  enrex  11133  axcnex  11213  zexALT  12694  cnexALT  13095  mpoaddex  13097  addex  13098  mpomulex  13099  mulex  13100  ixxex  13468  shftfval  15203  climconst2  15695  cpnnen  16377  ruclem13  16390  cnso  16395  prdsplusg  17609  prdsmulr  17610  prdsvsca  17611  prdsle  17613  prdshom  17618  prdsco  17619  xrsle  17756  fnmrc  17761  mrcfval  17762  mreacs  17812  comfffval  17852  oppccofval  17870  sectfval  17906  brssc  17969  sscpwex  17970  isssc  17975  isfunc  18019  isfuncd  18020  idfu2nd  18032  idfu1st  18034  idfucl  18036  wunfunc  18056  fuccofval  18117  homafval  18184  homaf  18185  homaval  18186  coapm  18226  catccofval  18259  catcfuccl  18273  xpcval  18331  xpcbas  18332  xpchom  18334  xpccofval  18336  1stfval  18345  2ndfval  18348  1stfcl  18351  2ndfcl  18352  catcxpccl  18361  evlf2  18372  evlf1  18374  evlfcl  18376  hof1fval  18407  hof2fval  18409  hofcl  18413  ipoval  18684  letsr  18747  frmdplusg  19030  smndex1gbas  19078  smndex1gid  19080  smndex1igid  19082  eqgfval  19368  efglem  19910  efgval  19911  cnfldds  21670  cnfldfun  21672  cnfldfunALT  21673  xrsadd  21676  xrsmul  21677  xrsds  21696  pzriprnglem13  21779  pzriprnglem14  21780  znle  21822  pjfval  21992  psrplusg  22225  ltbval  22332  opsrle  22336  evlslem2  22368  evlsvvval  22382  evlssca  22383  mpfind  22404  psdmul  22467  evls1sca  22621  pf1ind  22653  mat1dimmul  22771  2ndcctbss  23754  txuni2  23864  txbas  23866  eltx  23867  txcnp  23919  txcnmpt  23923  txrest  23930  txlm  23947  tx1stc  23949  tx2ndc  23950  txkgen  23951  txflf  24305  cnextfval  24361  distgp  24398  indistgp  24399  ustfn  24501  ustn0  24520  ussid  24559  ressuss  24561  ishtpy  25273  isphtpc  25295  elovolmlem  25775  dyadmbl  25901  vitali  25914  mbfimaopnlem  25956  dvfval  26197  plyeq0lem  26509  taylfval  26668  ulmval  26689  dmarea  27267  dchrplusg  27556  addsval  28330  mulsval  28477  zsex  28748  istrkg2ld  28904  tgjustc1  28919  tgjustc2  28920  iscgrg  28957  ishlg2  29047  ishlg  29050  ishpg  29219  iscgra  29298  isinag  29339  isleag  29348  axlowdimlem15  29516  axlowdim  29521  isgrpoi  31082  sspval  31307  0ofval  31371  ajfval  31393  hvmulex  31595  padct  33292  gsumwrd2dccat  33621  inftmrel  33723  isinftm  33724  smatrcl  34410  tpr2rico  34526  faeval  34861  mbfmco2  34880  br2base  34884  sxbrsigalem0  34886  sxbrsigalem3  34887  dya2iocrfn  34894  dya2iocct  34895  dya2iocnrect  34896  dya2iocuni  34898  dya2iocucvr  34899  sxbrsigalem2  34901  eulerpartlemgs2  34995  ccatmulgnn0dir  35157  afsval  35286  cvmlift2lem9  36045  satfv0  36092  satf00  36108  prv1n  36165  mexval  36236  mdvval  36238  mpstval  36269  brimg  36669  brrestrict  36683  colinearex  36795  nmulprop  36909  poimirlem4  38510  poimirlem28  38534  mblfinlem1  38543  heiborlem3  38715  rrnval  38729  ismrer1  38740  dfcnvrefrels2  39508  dfcnvrefrels3  39509  lcvfbr  40045  cmtfvalN  40235  cvrfval  40293  dvhvbase  42112  dvhfvadd  42116  dvhfvsca  42125  dibval  42167  dibfna  42179  dicval  42201  hdmap1fval  42821  ltex  43264  leex  43265  subex  43266  mzpincl  43698  pellexlem3  43791  pellexlem4  43792  pellexlem5  43793  aomclem6  44019  trclexi  44579  rtrclexi  44580  brtrclfv2  44686  mnringmulrcld  45185  hoiprodcl2  47509  hoicvrrex  47510  ovn0lem  47519  ovnhoilem1  47555  ovnlecvr2  47564  opnvonmbllem1  47586  opnvonmbllem2  47587  ovolval2lem  47597  ovolval2  47598  ovolval3  47601  ovolval4lem2  47604  ovolval5lem2  47607  ovnovollem1  47610  ovnovollem2  47611  gpgvtx  49085  gpgiedg  49086  sectfn  50081  nelsubc3  50123  cofidvala  50168  cofidval  50171  diag1f1lem  50358  fucoelvv  50372  fucofvalne  50377  functhinclem1  50496  functhinclem3  50498  functermc2  50561  idfudiag1bas  50576  idfudiag1  50577  prstchomval  50611  elpglem3  50750  pgindnf  50753  aacllem  50883