Theorem xpex 7745

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  oprabex  7973  oprabex3  7974  mpoexw  8075  naddcllem  8686  fnpm  8846  mapsnf1o2  8906  ixpsnf1o  8950  xpsnen  9067  endisj  9070  xpcomen  9075  xpassen  9078  xpmapenlem  9156  unxpdomlem3  9258  hartogslem1  9554  rankxpl  9887  rankfu  9889  rankmapu  9890  rankxplim  9891  rankxplim2  9892  rankxplim3  9893  rankxpsuc  9894  r0weon  10024  infxpenlem  10025  infxpenc2lem2  10032  dfac3  10133  dfac5lem2  10136  dfac5lem3  10137  dfac5lem4  10138  dfac5lem4OLD  10140  unctb  10216  axcc2lem  10448  axdc3lem  10462  axdc4lem  10467  enqex  10934  nqex  10935  nrex1  11076  enrex  11079  axcnex  11159  zexALT  12606  cnexALT  13000  mpoaddex  13002  addex  13003  mpomulex  13004  mulex  13005  ixxex  13371  shftfval  15087  climconst2  15562  cpnnen  16245  ruclem13  16258  cnso  16263  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdsle  17474  prdshom  17479  prdsco  17480  fnmrc  17617  mrcfval  17618  mreacs  17668  comfffval  17708  oppccofval  17726  sectfval  17762  brssc  17825  sscpwex  17826  isssc  17831  isfunc  17875  isfuncd  17876  idfu2nd  17888  idfu1st  17890  idfucl  17892  wunfunc  17912  fuccofval  17973  homafval  18040  homaf  18041  homaval  18042  coapm  18082  catccofval  18115  catcfuccl  18129  xpcval  18187  xpcbas  18188  xpchom  18190  xpccofval  18192  1stfval  18201  2ndfval  18204  1stfcl  18207  2ndfcl  18208  catcxpccl  18217  evlf2  18228  evlf1  18230  evlfcl  18232  hof1fval  18263  hof2fval  18265  hofcl  18269  ipoval  18538  letsr  18601  frmdplusg  18830  eqgfval  19157  efglem  19695  efgval  19696  cnfldds  21325  cnfldfun  21327  cnfldfunALT  21328  cnflddsOLD  21338  cnfldfunOLD  21340  cnfldfunALTOLD  21341  xrsadd  21345  xrsmul  21346  xrsle  21348  xrsds  21375  pzriprnglem13  21452  pzriprnglem14  21453  znle  21495  pjfval  21664  psrplusg  21894  ltbval  21999  opsrle  22003  evlslem2  22035  evlssca  22045  mpfind  22063  psdmul  22102  evls1sca  22259  pf1ind  22291  mat1dimmul  22412  2ndcctbss  23391  txuni2  23501  txbas  23503  eltx  23504  txcnp  23556  txcnmpt  23560  txrest  23567  txlm  23584  tx1stc  23586  tx2ndc  23587  txkgen  23588  txflf  23942  cnextfval  23998  distgp  24035  indistgp  24036  ustfn  24138  ustn0  24157  ussid  24197  ressuss  24199  ishtpy  24920  isphtpc  24942  elovolmlem  25425  dyadmbl  25551  vitali  25564  mbfimaopnlem  25606  dvfval  25848  plyeq0lem  26165  taylfval  26316  ulmval  26339  dmarea  26917  dchrplusg  27208  madefi  27867  addsval  27912  mulsval  28052  zsex  28283  tgjustc1  28400  tgjustc2  28401  iscgrg  28437  ishlg  28527  ishpg  28684  iscgra  28734  isinag  28763  isleag  28772  axlowdimlem15  28881  axlowdim  28886  isgrpoi  30425  sspval  30650  0ofval  30714  ajfval  30736  hvmulex  30938  gsumwrd2dccat  33007  inftmrel  33124  isinftm  33125  smatrcl  33773  tpr2rico  33889  faeval  34223  mbfmco2  34243  br2base  34247  sxbrsigalem0  34249  sxbrsigalem3  34250  dya2iocrfn  34257  dya2iocct  34258  dya2iocnrect  34259  dya2iocuni  34261  dya2iocucvr  34262  sxbrsigalem2  34264  eulerpartlemgs2  34358  ccatmulgnn0dir  34520  afsval  34649  cvmlift2lem9  35279  satfv0  35326  satf00  35342  prv1n  35399  mexval  35470  mdvval  35472  mpstval  35503  brimg  35901  brrestrict  35913  colinearex  36024  poimirlem4  37594  poimirlem28  37618  mblfinlem1  37627  heiborlem3  37783  rrnval  37797  ismrer1  37808  dfcnvrefrels2  38492  dfcnvrefrels3  38493  lcvfbr  38984  cmtfvalN  39174  cvrfval  39232  dvhvbase  41052  dvhfvadd  41056  dvhfvsca  41065  dibval  41107  dibfna  41119  dicval  41141  hdmap1fval  41761  ltex  42243  leex  42244  subex  42245  evlsvvval  42533  mzpincl  42704  pellexlem3  42801  pellexlem4  42802  pellexlem5  42803  aomclem6  43030  trclexi  43591  rtrclexi  43592  brtrclfv2  43698  mnringmulrcld  44200  hoiprodcl2  46532  hoicvrrex  46533  ovn0lem  46542  ovnhoilem1  46578  ovnlecvr2  46587  opnvonmbllem1  46609  opnvonmbllem2  46610  ovolval2lem  46620  ovolval2  46621  ovolval3  46624  ovolval4lem2  46627  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  smflimlem6  46753  gpgvtx  47995  gpgiedg  47996  sectfn  48947  nelsubc3  48986  diag1f1lem  49165  fucoelvv  49179  fucofvalne  49184  functhinclem1  49278  functhinclem3  49280  functermc2  49342  idfudiag1bas  49357  idfudiag1  49358  prstchomval  49384  elpglem3  49525  pgindnf  49528  aacllem  49613