Theorem xpex 7703

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-opab 5142  df-xp 5631  df-rel 5632

This theorem is referenced by:  oprabex  7925  oprabex3  7926  mpoexw  8027  naddcllem  8609  fnpm  8778  mapsnf1o2  8839  ixpsnf1o  8883  xpsnen  8996  endisj  8999  xpcomen  9003  xpassen  9006  xpmapenlem  9079  unxpdomlem3  9165  hartogslem1  9454  rankxpl  9797  rankfu  9799  rankmapu  9800  rankxplim  9801  rankxplim2  9802  rankxplim3  9803  rankxpsuc  9804  r0weon  9932  infxpenlem  9933  infxpenc2lem2  9940  dfac3  10041  dfac5lem2  10044  dfac5lem3  10045  dfac5lem4  10046  dfac5lem4OLD  10048  unctb  10124  axcc2lem  10356  axdc3lem  10370  axdc4lem  10375  enqex  10843  nqex  10844  nrex1  10985  enrex  10988  axcnex  11068  zexALT  12542  cnexALT  12934  mpoaddex  12936  addex  12937  mpomulex  12938  mulex  12939  ixxex  13307  shftfval  15030  climconst2  15508  cpnnen  16194  ruclem13  16207  cnso  16212  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  prdsle  17423  prdshom  17428  prdsco  17429  xrsle  17566  fnmrc  17571  mrcfval  17572  mreacs  17622  comfffval  17662  oppccofval  17680  sectfval  17716  brssc  17779  sscpwex  17780  isssc  17785  isfunc  17829  isfuncd  17830  idfu2nd  17842  idfu1st  17844  idfucl  17846  wunfunc  17866  fuccofval  17927  homafval  17994  homaf  17995  homaval  17996  coapm  18036  catccofval  18069  catcfuccl  18083  xpcval  18141  xpcbas  18142  xpchom  18144  xpccofval  18146  1stfval  18155  2ndfval  18158  1stfcl  18161  2ndfcl  18162  catcxpccl  18171  evlf2  18182  evlf1  18184  evlfcl  18186  hof1fval  18217  hof2fval  18219  hofcl  18223  ipoval  18494  letsr  18557  frmdplusg  18820  smndex1gbas  18868  smndex1gid  18870  smndex1igid  18872  eqgfval  19149  efglem  19689  efgval  19690  cnfldds  21366  cnfldfun  21368  cnfldfunALT  21369  xrsadd  21372  xrsmul  21373  xrsds  21392  pzriprnglem13  21475  pzriprnglem14  21476  znle  21518  pjfval  21688  psrplusg  21919  ltbval  22026  opsrle  22030  evlslem2  22062  evlsvvval  22076  evlssca  22077  mpfind  22098  psdmul  22161  evls1sca  22316  pf1ind  22348  mat1dimmul  22466  2ndcctbss  23445  txuni2  23555  txbas  23557  eltx  23558  txcnp  23610  txcnmpt  23614  txrest  23621  txlm  23638  tx1stc  23640  tx2ndc  23641  txkgen  23642  txflf  23996  cnextfval  24052  distgp  24089  indistgp  24090  ustfn  24192  ustn0  24211  ussid  24250  ressuss  24252  ishtpy  24964  isphtpc  24986  elovolmlem  25466  dyadmbl  25592  vitali  25605  mbfimaopnlem  25647  dvfval  25889  plyeq0lem  26200  taylfval  26349  ulmval  26370  dmarea  26946  dchrplusg  27235  madefi  27930  addsval  27979  mulsval  28126  zsex  28397  istrkg2ld  28553  tgjustc1  28568  tgjustc2  28569  iscgrg  28605  ishlg  28695  ishpg  28852  iscgra  28902  isinag  28931  isleag  28940  axlowdimlem15  29050  axlowdim  29055  isgrpoi  30594  sspval  30819  0ofval  30883  ajfval  30905  hvmulex  31107  padct  32817  gsumwrd2dccat  33166  inftmrel  33268  isinftm  33269  smatrcl  33987  tpr2rico  34103  faeval  34437  mbfmco2  34456  br2base  34460  sxbrsigalem0  34462  sxbrsigalem3  34463  dya2iocrfn  34470  dya2iocct  34471  dya2iocnrect  34472  dya2iocuni  34474  dya2iocucvr  34475  sxbrsigalem2  34477  eulerpartlemgs2  34571  ccatmulgnn0dir  34733  afsval  34862  cvmlift2lem9  35546  satfv0  35593  satf00  35609  prv1n  35666  mexval  35737  mdvval  35739  mpstval  35770  brimg  36170  brrestrict  36184  colinearex  36295  poimirlem4  37998  poimirlem28  38022  mblfinlem1  38031  heiborlem3  38187  rrnval  38201  ismrer1  38212  dfcnvrefrels2  38982  dfcnvrefrels3  38983  lcvfbr  39519  cmtfvalN  39709  cvrfval  39767  dvhvbase  41586  dvhfvadd  41590  dvhfvsca  41599  dibval  41641  dibfna  41653  dicval  41675  hdmap1fval  42295  ltex  42736  leex  42737  subex  42738  mzpincl  43190  pellexlem3  43283  pellexlem4  43284  pellexlem5  43285  aomclem6  43511  trclexi  44071  rtrclexi  44072  brtrclfv2  44178  mnringmulrcld  44679  hoiprodcl2  47005  hoicvrrex  47006  ovn0lem  47015  ovnhoilem1  47051  ovnlecvr2  47060  opnvonmbllem1  47082  opnvonmbllem2  47083  ovolval2lem  47093  ovolval2  47094  ovolval3  47097  ovolval4lem2  47100  ovolval5lem2  47103  ovnovollem1  47106  ovnovollem2  47107  smflimlem6  47226  gpgvtx  48541  gpgiedg  48542  sectfn  49526  nelsubc3  49568  cofidvala  49613  cofidval  49616  diag1f1lem  49803  fucoelvv  49817  fucofvalne  49822  functhinclem1  49941  functhinclem3  49943  functermc2  50006  idfudiag1bas  50021  idfudiag1  50022  prstchomval  50056  elpglem3  50210  pgindnf  50213  aacllem  50298