Theorem xpex 7771

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  oprabex  7999  oprabex3  8000  mpoexw  8101  naddcllem  8712  fnpm  8872  mapsnf1o2  8932  ixpsnf1o  8976  xpsnen  9093  endisj  9096  xpcomen  9101  xpassen  9104  xpmapenlem  9182  unxpdomlem3  9285  hartogslem1  9579  rankxpl  9912  rankfu  9914  rankmapu  9915  rankxplim  9916  rankxplim2  9917  rankxplim3  9918  rankxpsuc  9919  r0weon  10049  infxpenlem  10050  infxpenc2lem2  10057  dfac3  10158  dfac5lem2  10161  dfac5lem3  10162  dfac5lem4  10163  dfac5lem4OLD  10165  unctb  10241  axcc2lem  10473  axdc3lem  10487  axdc4lem  10492  enqex  10959  nqex  10960  nrex1  11101  enrex  11104  axcnex  11184  zexALT  12630  cnexALT  13025  mpoaddex  13027  addex  13028  mpomulex  13029  mulex  13030  ixxex  13394  shftfval  15105  climconst2  15580  cpnnen  16261  ruclem13  16274  cnso  16279  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdsle  17508  prdshom  17513  prdsco  17514  fnmrc  17651  mrcfval  17652  mreacs  17702  comfffval  17742  oppccofval  17761  sectfval  17798  brssc  17861  sscpwex  17862  isssc  17867  isfunc  17914  isfuncd  17915  idfu2nd  17927  idfu1st  17929  idfucl  17931  wunfunc  17951  wunfuncOLD  17952  fuccofval  18014  homafval  18082  homaf  18083  homaval  18084  coapm  18124  catccofval  18157  catcfuccl  18172  catcfucclOLD  18173  xpcval  18232  xpcbas  18233  xpchom  18235  xpccofval  18237  1stfval  18246  2ndfval  18249  1stfcl  18252  2ndfcl  18253  catcxpccl  18262  catcxpcclOLD  18263  evlf2  18274  evlf1  18276  evlfcl  18278  hof1fval  18309  hof2fval  18311  hofcl  18315  ipoval  18587  letsr  18650  frmdplusg  18879  eqgfval  19206  efglem  19748  efgval  19749  cnfldds  21393  cnfldfun  21395  cnfldfunALT  21396  cnflddsOLD  21406  cnfldfunOLD  21408  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  xrsadd  21414  xrsmul  21415  xrsle  21417  xrsds  21444  pzriprnglem13  21521  pzriprnglem14  21522  znle  21568  pjfval  21743  psrplusg  21973  ltbval  22078  opsrle  22082  evlslem2  22120  evlssca  22130  mpfind  22148  psdmul  22187  evls1sca  22342  pf1ind  22374  mat1dimmul  22497  2ndcctbss  23478  txuni2  23588  txbas  23590  eltx  23591  txcnp  23643  txcnmpt  23647  txrest  23654  txlm  23671  tx1stc  23673  tx2ndc  23674  txkgen  23675  txflf  24029  cnextfval  24085  distgp  24122  indistgp  24123  ustfn  24225  ustn0  24244  ussid  24284  ressuss  24286  ishtpy  25017  isphtpc  25039  elovolmlem  25522  dyadmbl  25648  vitali  25661  mbfimaopnlem  25703  dvfval  25946  plyeq0lem  26263  taylfval  26414  ulmval  26437  dmarea  27014  dchrplusg  27305  madefi  27964  addsval  28009  mulsval  28149  zsex  28380  tgjustc1  28497  tgjustc2  28498  iscgrg  28534  ishlg  28624  ishpg  28781  iscgra  28831  isinag  28860  isleag  28869  axlowdimlem15  28985  axlowdim  28990  isgrpoi  30526  sspval  30751  0ofval  30815  ajfval  30837  hvmulex  31039  gsumwrd2dccat  33052  inftmrel  33169  isinftm  33170  smatrcl  33756  tpr2rico  33872  faeval  34226  mbfmco2  34246  br2base  34250  sxbrsigalem0  34252  sxbrsigalem3  34253  dya2iocrfn  34260  dya2iocct  34261  dya2iocnrect  34262  dya2iocuni  34264  dya2iocucvr  34265  sxbrsigalem2  34267  eulerpartlemgs2  34361  ccatmulgnn0dir  34535  afsval  34664  cvmlift2lem9  35295  satfv0  35342  satf00  35358  prv1n  35415  mexval  35486  mdvval  35488  mpstval  35519  brimg  35918  brrestrict  35930  colinearex  36041  poimirlem4  37610  poimirlem28  37634  mblfinlem1  37643  heiborlem3  37799  rrnval  37813  ismrer1  37824  dfcnvrefrels2  38509  dfcnvrefrels3  38510  lcvfbr  39001  cmtfvalN  39191  cvrfval  39249  dvhvbase  41069  dvhfvadd  41073  dvhfvsca  41082  dibval  41124  dibfna  41136  dicval  41158  hdmap1fval  41778  ltex  42264  leex  42265  subex  42266  evlsvvval  42549  mzpincl  42721  pellexlem3  42818  pellexlem4  42819  pellexlem5  42820  aomclem6  43047  trclexi  43609  rtrclexi  43610  brtrclfv2  43716  mnringmulrcld  44223  hoiprodcl2  46510  hoicvrrex  46511  ovn0lem  46520  ovnhoilem1  46556  ovnlecvr2  46565  opnvonmbllem1  46587  opnvonmbllem2  46588  ovolval2lem  46598  ovolval2  46599  ovolval3  46602  ovolval4lem2  46605  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  smflimlem6  46731  gpgvtx  47937  gpgiedg  47938  functhinclem1  48840  functhinclem3  48842  prstchomval  48874  elpglem3  48943  pgindnf  48946  aacllem  49031