Theorem xpex 7740

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

Syntax hints:   ∈ wcel 2145  Vcvv 3457   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-opab 5168  df-xp 5658  df-rel 5659

This theorem is referenced by:  oprabex  7961  oprabex3  7962  mpoexw  8063  naddcllem  8650  fnpm  8819  mapsnf1o2  8880  ixpsnf1o  8924  xpsnen  9037  endisj  9040  xpcomen  9044  xpassen  9047  xpmapenlem  9120  unxpdomlem3  9206  hartogslem1  9492  rankxpl  9835  rankfu  9837  rankmapu  9838  rankxplim  9839  rankxplim2  9840  rankxplim3  9841  rankxpsuc  9842  r0weon  9984  infxpenlem  9985  infxpenc2lem2  9992  dfac3  10093  dfac5lem2  10096  dfac5lem3  10097  dfac5lem4  10098  unctb  10175  axcc2lem  10408  axdc3lem  10422  axdc4lem  10427  enqex  10895  nqex  10896  nrex1  11037  enrex  11040  axcnex  11120  zexALT  12602  cnexALT  13001  mpoaddex  13003  addex  13004  mpomulex  13005  mulex  13006  ixxex  13374  shftfval  15097  climconst2  15589  cpnnen  16275  ruclem13  16288  cnso  16293  prdsplusg  17501  prdsmulr  17502  prdsvsca  17503  prdsle  17505  prdshom  17510  prdsco  17511  xrsle  17648  fnmrc  17653  mrcfval  17654  mreacs  17704  comfffval  17744  oppccofval  17762  sectfval  17798  brssc  17861  sscpwex  17862  isssc  17867  isfunc  17911  isfuncd  17912  idfu2nd  17924  idfu1st  17926  idfucl  17928  wunfunc  17948  fuccofval  18009  homafval  18076  homaf  18077  homaval  18078  coapm  18118  catccofval  18151  catcfuccl  18165  xpcval  18223  xpcbas  18224  xpchom  18226  xpccofval  18228  1stfval  18237  2ndfval  18240  1stfcl  18243  2ndfcl  18244  catcxpccl  18253  evlf2  18264  evlf1  18266  evlfcl  18268  hof1fval  18299  hof2fval  18301  hofcl  18305  ipoval  18576  letsr  18639  frmdplusg  18903  smndex1gbas  18951  smndex1gid  18953  smndex1igid  18955  eqgfval  19235  efglem  19777  efgval  19778  cnfldds  21494  cnfldfun  21496  cnfldfunALT  21497  xrsadd  21500  xrsmul  21501  xrsds  21520  pzriprnglem13  21603  pzriprnglem14  21604  znle  21646  pjfval  21816  psrplusg  22047  ltbval  22154  opsrle  22158  evlslem2  22190  evlsvvval  22204  evlssca  22205  mpfind  22226  psdmul  22289  evls1sca  22444  pf1ind  22476  mat1dimmul  22594  2ndcctbss  23573  txuni2  23683  txbas  23685  eltx  23686  txcnp  23738  txcnmpt  23742  txrest  23749  txlm  23766  tx1stc  23768  tx2ndc  23769  txkgen  23770  txflf  24124  cnextfval  24180  distgp  24217  indistgp  24218  ustfn  24320  ustn0  24339  ussid  24378  ressuss  24380  ishtpy  25092  isphtpc  25114  elovolmlem  25594  dyadmbl  25720  vitali  25733  mbfimaopnlem  25775  dvfval  26017  plyeq0lem  26328  taylfval  26480  ulmval  26501  dmarea  27080  dchrplusg  27369  madefi  28064  addsval  28113  mulsval  28260  zsex  28531  istrkg2ld  28687  tgjustc1  28702  tgjustc2  28703  iscgrg  28739  ishlg  28829  ishpg  28990  iscgra  29061  isinag  29090  isleag  29099  axlowdimlem15  29215  axlowdim  29220  isgrpoi  30759  sspval  30984  0ofval  31048  ajfval  31070  hvmulex  31272  padct  32975  gsumwrd2dccat  33311  inftmrel  33413  isinftm  33414  smatrcl  34103  tpr2rico  34219  faeval  34553  mbfmco2  34572  br2base  34576  sxbrsigalem0  34578  sxbrsigalem3  34579  dya2iocrfn  34586  dya2iocct  34587  dya2iocnrect  34588  dya2iocuni  34590  dya2iocucvr  34591  sxbrsigalem2  34593  eulerpartlemgs2  34687  ccatmulgnn0dir  34849  afsval  34978  cvmlift2lem9  35674  satfv0  35721  satf00  35737  prv1n  35794  mexval  35865  mdvval  35867  mpstval  35898  brimg  36298  brrestrict  36312  colinearex  36423  nmulprop  36553  poimirlem4  38135  poimirlem28  38159  mblfinlem1  38168  heiborlem3  38324  rrnval  38338  ismrer1  38349  dfcnvrefrels2  39119  dfcnvrefrels3  39120  lcvfbr  39656  cmtfvalN  39846  cvrfval  39904  dvhvbase  41723  dvhfvadd  41727  dvhfvsca  41736  dibval  41778  dibfna  41790  dicval  41812  hdmap1fval  42432  ltex  42873  leex  42874  subex  42875  mzpincl  43327  pellexlem3  43420  pellexlem4  43421  pellexlem5  43422  aomclem6  43648  trclexi  44208  rtrclexi  44209  brtrclfv2  44315  mnringmulrcld  44816  hoiprodcl2  47127  hoicvrrex  47128  ovn0lem  47137  ovnhoilem1  47173  ovnlecvr2  47182  opnvonmbllem1  47204  opnvonmbllem2  47205  ovolval2lem  47215  ovolval2  47216  ovolval3  47219  ovolval4lem2  47222  ovolval5lem2  47225  ovnovollem1  47228  ovnovollem2  47229  smflimlem6  47348  gpgvtx  48663  gpgiedg  48664  sectfn  49658  nelsubc3  49700  cofidvala  49745  cofidval  49748  diag1f1lem  49935  fucoelvv  49949  fucofvalne  49954  functhinclem1  50073  functhinclem3  50075  functermc2  50138  idfudiag1bas  50153  idfudiag1  50154  prstchomval  50188  elpglem3  50342  pgindnf  50345  aacllem  50430