Theorem xpex 7788

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  oprabex  8017  oprabex3  8018  mpoexw  8119  naddcllem  8732  fnpm  8892  mapsnf1o2  8952  ixpsnf1o  8996  xpsnen  9121  endisj  9124  xpcomen  9129  xpassen  9132  xpmapenlem  9210  unxpdomlem3  9315  hartogslem1  9611  rankxpl  9944  rankfu  9946  rankmapu  9947  rankxplim  9948  rankxplim2  9949  rankxplim3  9950  rankxpsuc  9951  r0weon  10081  infxpenlem  10082  infxpenc2lem2  10089  dfac3  10190  dfac5lem2  10193  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  unctb  10273  axcc2lem  10505  axdc3lem  10519  axdc4lem  10524  enqex  10991  nqex  10992  nrex1  11133  enrex  11136  axcnex  11216  zexALT  12659  cnexALT  13051  mpoaddex  13053  addex  13054  mpomulex  13055  mulex  13056  ixxex  13418  shftfval  15119  climconst2  15594  cpnnen  16277  ruclem13  16290  cnso  16295  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdsle  17522  prdshom  17527  prdsco  17528  fnmrc  17665  mrcfval  17666  mreacs  17716  comfffval  17756  oppccofval  17775  sectfval  17812  brssc  17875  sscpwex  17876  isssc  17881  isfunc  17928  isfuncd  17929  idfu2nd  17941  idfu1st  17943  idfucl  17945  wunfunc  17965  wunfuncOLD  17966  fuccofval  18028  homafval  18096  homaf  18097  homaval  18098  coapm  18138  catccofval  18171  catcfuccl  18186  catcfucclOLD  18187  xpcval  18246  xpcbas  18247  xpchom  18249  xpccofval  18251  1stfval  18260  2ndfval  18263  1stfcl  18266  2ndfcl  18267  catcxpccl  18276  catcxpcclOLD  18277  evlf2  18288  evlf1  18290  evlfcl  18292  hof1fval  18323  hof2fval  18325  hofcl  18329  ipoval  18600  letsr  18663  frmdplusg  18889  eqgfval  19216  efglem  19758  efgval  19759  cnfldds  21399  cnfldfun  21401  cnfldfunALT  21402  cnflddsOLD  21412  cnfldfunOLD  21414  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  xrsadd  21420  xrsmul  21421  xrsle  21423  xrsds  21450  pzriprnglem13  21527  pzriprnglem14  21528  znle  21574  pjfval  21749  psrplusg  21979  ltbval  22084  opsrle  22088  evlslem2  22126  evlssca  22136  mpfind  22154  psdmul  22193  evls1sca  22348  pf1ind  22380  mat1dimmul  22503  2ndcctbss  23484  txuni2  23594  txbas  23596  eltx  23597  txcnp  23649  txcnmpt  23653  txrest  23660  txlm  23677  tx1stc  23679  tx2ndc  23680  txkgen  23681  txflf  24035  cnextfval  24091  distgp  24128  indistgp  24129  ustfn  24231  ustn0  24250  ussid  24290  ressuss  24292  ishtpy  25023  isphtpc  25045  elovolmlem  25528  dyadmbl  25654  vitali  25667  mbfimaopnlem  25709  dvfval  25952  plyeq0lem  26269  taylfval  26418  ulmval  26441  dmarea  27018  dchrplusg  27309  madefi  27968  addsval  28013  mulsval  28153  zsex  28384  tgjustc1  28501  tgjustc2  28502  iscgrg  28538  ishlg  28628  ishpg  28785  iscgra  28835  isinag  28864  isleag  28873  axlowdimlem15  28989  axlowdim  28994  isgrpoi  30530  sspval  30755  0ofval  30819  ajfval  30841  hvmulex  31043  inftmrel  33160  isinftm  33161  smatrcl  33742  tpr2rico  33858  faeval  34210  mbfmco2  34230  br2base  34234  sxbrsigalem0  34236  sxbrsigalem3  34237  dya2iocrfn  34244  dya2iocct  34245  dya2iocnrect  34246  dya2iocuni  34248  dya2iocucvr  34249  sxbrsigalem2  34251  eulerpartlemgs2  34345  ccatmulgnn0dir  34519  afsval  34648  cvmlift2lem9  35279  satfv0  35326  satf00  35342  prv1n  35399  mexval  35470  mdvval  35472  mpstval  35503  brimg  35901  brrestrict  35913  colinearex  36024  poimirlem4  37584  poimirlem28  37608  mblfinlem1  37617  heiborlem3  37773  rrnval  37787  ismrer1  37798  dfcnvrefrels2  38484  dfcnvrefrels3  38485  lcvfbr  38976  cmtfvalN  39166  cvrfval  39224  dvhvbase  41044  dvhfvadd  41048  dvhfvsca  41057  dibval  41099  dibfna  41111  dicval  41133  hdmap1fval  41753  ltex  42240  leex  42241  subex  42242  evlsvvval  42518  mzpincl  42690  pellexlem3  42787  pellexlem4  42788  pellexlem5  42789  aomclem6  43016  trclexi  43582  rtrclexi  43583  brtrclfv2  43689  mnringmulrcld  44197  hoiprodcl2  46476  hoicvrrex  46477  ovn0lem  46486  ovnhoilem1  46522  ovnlecvr2  46531  opnvonmbllem1  46553  opnvonmbllem2  46554  ovolval2lem  46564  ovolval2  46565  ovolval3  46568  ovolval4lem2  46571  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  smflimlem6  46697  functhinclem1  48708  functhinclem3  48710  prstchomval  48741  elpglem3  48805  pgindnf  48808  aacllem  48895