Theorem xpex 7756

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  oprabex  7977  oprabex3  7978  mpoexw  8081  naddcllem  8668  fnpm  8837  mapsnf1o2  8905  ixpsnf1o  8949  xpsnen  9063  endisj  9066  xpcomen  9070  xpassen  9073  xpmapenlem  9146  unxpdomlem3  9232  hartogslem1  9518  rankxpl  9861  rankfu  9863  rankmapu  9864  rankxplim  9865  rankxplim2  9866  rankxplim3  9867  rankxpsuc  9868  r0weon  10019  infxpenlem  10020  infxpenc2lem2  10027  dfac3  10128  dfac5lem2  10131  dfac5lem3  10132  dfac5lem4  10133  unctb  10210  axcc2lem  10442  axdc3lem  10456  axdc4lem  10461  enqex  10935  nqex  10936  nrex1  11077  enrex  11080  axcnex  11160  zexALT  12639  cnexALT  13040  mpoaddex  13042  addex  13043  mpomulex  13044  mulex  13045  ixxex  13413  shftfval  15147  climconst2  15639  cpnnen  16323  ruclem13  16336  cnso  16341  prdsplusg  17549  prdsmulr  17550  prdsvsca  17551  prdsle  17553  prdshom  17558  prdsco  17559  xrsle  17696  fnmrc  17701  mrcfval  17702  mreacs  17752  comfffval  17792  oppccofval  17810  sectfval  17846  brssc  17909  sscpwex  17910  isssc  17915  isfunc  17959  isfuncd  17960  idfu2nd  17972  idfu1st  17974  idfucl  17976  wunfunc  17996  fuccofval  18057  homafval  18124  homaf  18125  homaval  18126  coapm  18166  catccofval  18199  catcfuccl  18213  xpcval  18271  xpcbas  18272  xpchom  18274  xpccofval  18276  1stfval  18285  2ndfval  18288  1stfcl  18291  2ndfcl  18292  catcxpccl  18301  evlf2  18312  evlf1  18314  evlfcl  18316  hof1fval  18347  hof2fval  18349  hofcl  18353  ipoval  18624  letsr  18687  frmdplusg  18969  smndex1gbas  19017  smndex1gid  19019  smndex1igid  19021  eqgfval  19307  efglem  19849  efgval  19850  cnfldds  21603  cnfldfun  21605  cnfldfunALT  21606  xrsadd  21609  xrsmul  21610  xrsds  21629  pzriprnglem13  21712  pzriprnglem14  21713  znle  21755  pjfval  21925  psrplusg  22158  ltbval  22265  opsrle  22269  evlslem2  22301  evlsvvval  22315  evlssca  22316  mpfind  22337  psdmul  22400  evls1sca  22554  pf1ind  22586  mat1dimmul  22704  2ndcctbss  23687  txuni2  23797  txbas  23799  eltx  23800  txcnp  23852  txcnmpt  23856  txrest  23863  txlm  23880  tx1stc  23882  tx2ndc  23883  txkgen  23884  txflf  24238  cnextfval  24294  distgp  24331  indistgp  24332  ustfn  24434  ustn0  24453  ussid  24492  ressuss  24494  ishtpy  25206  isphtpc  25228  elovolmlem  25708  dyadmbl  25834  vitali  25847  mbfimaopnlem  25889  dvfval  26131  plyeq0lem  26443  taylfval  26602  ulmval  26623  dmarea  27202  dchrplusg  27491  addsval  28235  mulsval  28382  zsex  28653  istrkg2ld  28809  tgjustc1  28824  tgjustc2  28825  iscgrg  28862  ishlg2  28952  ishlg  28955  ishpg  29124  iscgra  29203  isinag  29244  isleag  29253  axlowdimlem15  29421  axlowdim  29426  isgrpoi  30987  sspval  31212  0ofval  31276  ajfval  31298  hvmulex  31500  padct  33197  gsumwrd2dccat  33526  inftmrel  33628  isinftm  33629  smatrcl  34314  tpr2rico  34430  faeval  34765  mbfmco2  34784  br2base  34788  sxbrsigalem0  34790  sxbrsigalem3  34791  dya2iocrfn  34798  dya2iocct  34799  dya2iocnrect  34800  dya2iocuni  34802  dya2iocucvr  34803  sxbrsigalem2  34805  eulerpartlemgs2  34899  ccatmulgnn0dir  35061  afsval  35190  cvmlift2lem9  35898  satfv0  35945  satf00  35961  prv1n  36018  mexval  36089  mdvval  36091  mpstval  36122  brimg  36522  brrestrict  36536  colinearex  36648  nmulprop  36778  poimirlem4  38381  poimirlem28  38405  mblfinlem1  38414  heiborlem3  38571  rrnval  38585  ismrer1  38596  dfcnvrefrels2  39364  dfcnvrefrels3  39365  lcvfbr  39901  cmtfvalN  40091  cvrfval  40149  dvhvbase  41968  dvhfvadd  41972  dvhfvsca  41981  dibval  42023  dibfna  42035  dicval  42057  hdmap1fval  42677  ltex  43120  leex  43121  subex  43122  mzpincl  43587  pellexlem3  43680  pellexlem4  43681  pellexlem5  43682  aomclem6  43908  trclexi  44468  rtrclexi  44469  brtrclfv2  44575  mnringmulrcld  45074  hoiprodcl2  47391  hoicvrrex  47392  ovn0lem  47401  ovnhoilem1  47437  ovnlecvr2  47446  opnvonmbllem1  47468  opnvonmbllem2  47469  ovolval2lem  47479  ovolval2  47480  ovolval3  47483  ovolval4lem2  47486  ovolval5lem2  47489  ovnovollem1  47492  ovnovollem2  47493  gpgvtx  48967  gpgiedg  48968  sectfn  49963  nelsubc3  50005  cofidvala  50050  cofidval  50053  diag1f1lem  50240  fucoelvv  50254  fucofvalne  50259  functhinclem1  50378  functhinclem3  50380  functermc2  50443  idfudiag1bas  50458  idfudiag1  50459  prstchomval  50493  elpglem3  50647  pgindnf  50650  aacllem  50780