Theorem xpex 6962

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

Syntax hints:   ∈ wcel 1990  Vcvv 3200   × cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  oprabex  7156  oprabex3  7157  fnpm  7865  mapsnf1o2  7905  ixpsnf1o  7948  xpsnen  8044  endisj  8047  xpcomen  8051  xpassen  8054  xpmapenlem  8127  mapunen  8129  unxpdomlem3  8166  hartogslem1  8447  rankxpl  8738  rankfu  8740  rankmapu  8741  rankxplim  8742  rankxplim2  8743  rankxplim3  8744  rankxpsuc  8745  r0weon  8835  infxpenlem  8836  infxpenc2lem2  8843  dfac3  8944  dfac5lem2  8947  dfac5lem3  8948  dfac5lem4  8949  cdafn  8991  unctb  9027  axcc2lem  9258  axdc3lem  9272  axdc4lem  9277  enqex  9744  nqex  9745  enrex  9888  axcnex  9968  zexALT  11396  cnexALT  11828  addex  11830  mulex  11831  ixxex  12186  shftfval  13810  climconst2  14279  cpnnen  14958  ruclem13  14971  cnso  14976  prdsval  16115  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdsle  16122  prdsds  16124  prdshom  16127  prdsco  16128  fnmrc  16267  mrcfval  16268  mreacs  16319  comfffval  16358  oppccofval  16376  sectfval  16411  brssc  16474  sscpwex  16475  isssc  16480  isfunc  16524  isfuncd  16525  idfu2nd  16537  idfu1st  16539  idfucl  16541  wunfunc  16559  fuccofval  16619  homafval  16679  homaf  16680  homaval  16681  coapm  16721  catccofval  16750  catcfuccl  16759  xpcval  16817  xpcbas  16818  xpchom  16820  xpccofval  16822  1stfval  16831  2ndfval  16834  1stfcl  16837  2ndfcl  16838  catcxpccl  16847  evlf2  16858  evlf1  16860  evlfcl  16862  hof1fval  16893  hof2fval  16895  hofcl  16899  ipoval  17154  letsr  17227  plusffval  17247  frmdplusg  17391  eqgfval  17642  efglem  18129  efgval  18130  scaffval  18881  psrplusg  19381  ltbval  19471  opsrle  19475  evlslem2  19512  evlssca  19522  mpfind  19536  evls1sca  19688  pf1ind  19719  cnfldds  19756  cnfldfun  19758  cnfldfunALT  19759  xrsadd  19763  xrsmul  19764  xrsle  19766  xrsds  19789  znle  19884  ipffval  19993  pjfval  20050  mat1dimmul  20282  2ndcctbss  21258  txuni2  21368  txbas  21370  eltx  21371  txcnp  21423  txcnmpt  21427  txrest  21434  txlm  21451  tx1stc  21453  tx2ndc  21454  txkgen  21455  txflf  21810  cnextfval  21866  distgp  21903  indistgp  21904  ustfn  22005  ustn0  22024  ussid  22064  ressuss  22067  ishtpy  22771  isphtpc  22793  elovolm  23243  elovolmr  23244  ovolmge0  23245  ovolgelb  23248  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovolshftlem2  23278  ovolicc2  23290  ioombl1  23330  dyadmbl  23368  vitali  23382  mbfimaopnlem  23422  dvfval  23661  plyeq0lem  23966  taylfval  24113  ulmval  24134  dmarea  24684  dchrplusg  24972  iscgrg  25407  ishlg  25497  ishpg  25651  iscgra  25701  isinag  25729  axlowdimlem15  25836  axlowdim  25841  isgrpoi  27352  sspval  27578  0ofval  27642  ajfval  27664  hvmulex  27868  inftmrel  29734  isinftm  29735  smatrcl  29862  tpr2rico  29958  faeval  30309  mbfmco2  30327  br2base  30331  sxbrsigalem0  30333  sxbrsigalem3  30334  dya2iocrfn  30341  dya2iocct  30342  dya2iocnrect  30343  dya2iocuni  30345  dya2iocucvr  30346  sxbrsigalem2  30348  eulerpartlemgs2  30442  ccatmulgnn0dir  30619  afsval  30749  cvmlift2lem9  31293  mexval  31399  mdvval  31401  mpstval  31432  brimg  32044  brrestrict  32056  colinearex  32167  poimirlem4  33413  poimirlem28  33437  mblfinlem1  33446  heiborlem3  33612  rrnval  33626  ismrer1  33637  lcvfbr  34307  cmtfvalN  34497  cvrfval  34555  dvhvbase  36376  dvhfvadd  36380  dvhfvsca  36389  dibval  36431  dibfna  36443  dicval  36465  hdmap1fval  37086  mzpincl  37297  pellexlem3  37395  pellexlem4  37396  pellexlem5  37397  aomclem6  37629  trclexi  37927  rtrclexi  37928  brtrclfv2  38019  hoiprodcl2  40769  hoicvrrex  40770  ovn0lem  40779  ovnhoilem1  40815  ovnlecvr2  40824  opnvonmbllem1  40846  opnvonmbllem2  40847  ovolval2lem  40857  ovolval2  40858  ovolval3  40861  ovolval4lem2  40864  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  smflimlem6  40984  elpglem3  42456  aacllem  42547