Theorem xpex 7753

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-opab 5175  df-xp 5669  df-rel 5670

This theorem is referenced by:  oprabex  7974  oprabex3  7975  mpoexw  8076  naddcllem  8663  fnpm  8832  mapsnf1o2  8893  ixpsnf1o  8937  xpsnen  9050  endisj  9053  xpcomen  9057  xpassen  9060  xpmapenlem  9133  unxpdomlem3  9219  hartogslem1  9505  rankxpl  9848  rankfu  9850  rankmapu  9851  rankxplim  9852  rankxplim2  9853  rankxplim3  9854  rankxpsuc  9855  r0weon  9997  infxpenlem  9998  infxpenc2lem2  10005  dfac3  10106  dfac5lem2  10109  dfac5lem3  10110  dfac5lem4  10111  unctb  10188  axcc2lem  10421  axdc3lem  10435  axdc4lem  10440  enqex  10908  nqex  10909  nrex1  11050  enrex  11053  axcnex  11133  zexALT  12612  cnexALT  13011  mpoaddex  13013  addex  13014  mpomulex  13015  mulex  13016  ixxex  13384  shftfval  15109  climconst2  15601  cpnnen  16286  ruclem13  16299  cnso  16304  prdsplusg  17512  prdsmulr  17513  prdsvsca  17514  prdsle  17516  prdshom  17521  prdsco  17522  xrsle  17659  fnmrc  17664  mrcfval  17665  mreacs  17715  comfffval  17755  oppccofval  17773  sectfval  17809  brssc  17872  sscpwex  17873  isssc  17878  isfunc  17922  isfuncd  17923  idfu2nd  17935  idfu1st  17937  idfucl  17939  wunfunc  17959  fuccofval  18020  homafval  18087  homaf  18088  homaval  18089  coapm  18129  catccofval  18162  catcfuccl  18176  xpcval  18234  xpcbas  18235  xpchom  18237  xpccofval  18239  1stfval  18248  2ndfval  18251  1stfcl  18254  2ndfcl  18255  catcxpccl  18264  evlf2  18275  evlf1  18277  evlfcl  18279  hof1fval  18310  hof2fval  18312  hofcl  18316  ipoval  18587  letsr  18650  frmdplusg  18914  smndex1gbas  18962  smndex1gid  18964  smndex1igid  18966  eqgfval  19245  efglem  19787  efgval  19788  cnfldds  21515  cnfldfun  21517  cnfldfunALT  21518  xrsadd  21521  xrsmul  21522  xrsds  21541  pzriprnglem13  21624  pzriprnglem14  21625  znle  21667  pjfval  21837  psrplusg  22068  ltbval  22175  opsrle  22179  evlslem2  22211  evlsvvval  22225  evlssca  22226  mpfind  22247  psdmul  22310  evls1sca  22464  pf1ind  22496  mat1dimmul  22614  2ndcctbss  23593  txuni2  23703  txbas  23705  eltx  23706  txcnp  23758  txcnmpt  23762  txrest  23769  txlm  23786  tx1stc  23788  tx2ndc  23789  txkgen  23790  txflf  24144  cnextfval  24200  distgp  24237  indistgp  24238  ustfn  24340  ustn0  24359  ussid  24398  ressuss  24400  ishtpy  25112  isphtpc  25134  elovolmlem  25614  dyadmbl  25740  vitali  25753  mbfimaopnlem  25795  dvfval  26037  plyeq0lem  26348  taylfval  26503  ulmval  26524  dmarea  27103  dchrplusg  27392  madefi  28087  addsval  28136  mulsval  28283  zsex  28554  istrkg2ld  28710  tgjustc1  28725  tgjustc2  28726  iscgrg  28762  ishlg2  28852  ishlg  28855  ishpg  29022  iscgra  29101  isinag  29136  isleag  29145  axlowdimlem15  29287  axlowdim  29292  isgrpoi  30831  sspval  31056  0ofval  31120  ajfval  31142  hvmulex  31344  padct  33044  gsumwrd2dccat  33379  inftmrel  33481  isinftm  33482  smatrcl  34167  tpr2rico  34283  faeval  34617  mbfmco2  34636  br2base  34640  sxbrsigalem0  34642  sxbrsigalem3  34643  dya2iocrfn  34650  dya2iocct  34651  dya2iocnrect  34652  dya2iocuni  34654  dya2iocucvr  34655  sxbrsigalem2  34657  eulerpartlemgs2  34751  ccatmulgnn0dir  34913  afsval  35042  cvmlift2lem9  35784  satfv0  35831  satf00  35847  prv1n  35904  mexval  35975  mdvval  35977  mpstval  36008  brimg  36408  brrestrict  36422  colinearex  36533  nmulprop  36663  poimirlem4  38256  poimirlem28  38280  mblfinlem1  38289  heiborlem3  38445  rrnval  38459  ismrer1  38470  dfcnvrefrels2  39238  dfcnvrefrels3  39239  lcvfbr  39775  cmtfvalN  39965  cvrfval  40023  dvhvbase  41842  dvhfvadd  41846  dvhfvsca  41855  dibval  41897  dibfna  41909  dicval  41931  hdmap1fval  42551  ltex  42994  leex  42995  subex  42996  mzpincl  43448  pellexlem3  43541  pellexlem4  43542  pellexlem5  43543  aomclem6  43769  trclexi  44329  rtrclexi  44330  brtrclfv2  44436  mnringmulrcld  44935  hoiprodcl2  47252  hoicvrrex  47253  ovn0lem  47262  ovnhoilem1  47298  ovnlecvr2  47307  opnvonmbllem1  47329  opnvonmbllem2  47330  ovolval2lem  47340  ovolval2  47341  ovolval3  47344  ovolval4lem2  47347  ovolval5lem2  47350  ovnovollem1  47353  ovnovollem2  47354  smflimlem6  47473  gpgvtx  48791  gpgiedg  48792  sectfn  49790  nelsubc3  49832  cofidvala  49877  cofidval  49880  diag1f1lem  50067  fucoelvv  50081  fucofvalne  50086  functhinclem1  50205  functhinclem3  50207  functermc2  50270  idfudiag1bas  50285  idfudiag1  50286  prstchomval  50320  elpglem3  50474  pgindnf  50477  aacllem  50584