Theorem xpex 7761

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458   × cxp 5664

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-opab 5179  df-xp 5672  df-rel 5673

This theorem is used by:  oprabex  7982  oprabex3  7983  mpoexw  8084  naddcllem  8671  fnpm  8840  mapsnf1o2  8901  ixpsnf1o  8945  xpsnen  9059  endisj  9062  xpcomen  9066  xpassen  9069  xpmapenlem  9142  unxpdomlem3  9228  hartogslem1  9514  rankxpl  9857  rankfu  9859  rankmapu  9860  rankxplim  9861  rankxplim2  9862  rankxplim3  9863  rankxpsuc  9864  r0weon  10015  infxpenlem  10016  infxpenc2lem2  10023  dfac3  10124  dfac5lem2  10127  dfac5lem3  10128  dfac5lem4  10129  unctb  10206  axcc2lem  10438  axdc3lem  10452  axdc4lem  10457  enqex  10925  nqex  10926  nrex1  11067  enrex  11070  axcnex  11150  zexALT  12629  cnexALT  13028  mpoaddex  13030  addex  13031  mpomulex  13032  mulex  13033  ixxex  13401  shftfval  15133  climconst2  15625  cpnnen  16310  ruclem13  16323  cnso  16328  prdsplusg  17536  prdsmulr  17537  prdsvsca  17538  prdsle  17540  prdshom  17545  prdsco  17546  xrsle  17683  fnmrc  17688  mrcfval  17689  mreacs  17739  comfffval  17779  oppccofval  17797  sectfval  17833  brssc  17896  sscpwex  17897  isssc  17902  isfunc  17946  isfuncd  17947  idfu2nd  17959  idfu1st  17961  idfucl  17963  wunfunc  17983  fuccofval  18044  homafval  18111  homaf  18112  homaval  18113  coapm  18153  catccofval  18186  catcfuccl  18200  xpcval  18258  xpcbas  18259  xpchom  18261  xpccofval  18263  1stfval  18272  2ndfval  18275  1stfcl  18278  2ndfcl  18279  catcxpccl  18288  evlf2  18299  evlf1  18301  evlfcl  18303  hof1fval  18334  hof2fval  18336  hofcl  18340  ipoval  18611  letsr  18674  frmdplusg  18944  smndex1gbas  18992  smndex1gid  18994  smndex1igid  18996  eqgfval  19275  efglem  19817  efgval  19818  cnfldds  21571  cnfldfun  21573  cnfldfunALT  21574  xrsadd  21577  xrsmul  21578  xrsds  21597  pzriprnglem13  21680  pzriprnglem14  21681  znle  21723  pjfval  21893  psrplusg  22124  ltbval  22231  opsrle  22235  evlslem2  22267  evlsvvval  22281  evlssca  22282  mpfind  22303  psdmul  22366  evls1sca  22520  pf1ind  22552  mat1dimmul  22670  2ndcctbss  23649  txuni2  23759  txbas  23761  eltx  23762  txcnp  23814  txcnmpt  23818  txrest  23825  txlm  23842  tx1stc  23844  tx2ndc  23845  txkgen  23846  txflf  24200  cnextfval  24256  distgp  24293  indistgp  24294  ustfn  24396  ustn0  24415  ussid  24454  ressuss  24456  ishtpy  25168  isphtpc  25190  elovolmlem  25670  dyadmbl  25796  vitali  25809  mbfimaopnlem  25851  dvfval  26093  plyeq0lem  26404  taylfval  26559  ulmval  26580  dmarea  27159  dchrplusg  27448  madefi  28143  addsval  28192  mulsval  28339  zsex  28610  istrkg2ld  28766  tgjustc1  28781  tgjustc2  28782  iscgrg  28818  ishlg2  28908  ishlg  28911  ishpg  29078  iscgra  29157  isinag  29192  isleag  29201  axlowdimlem15  29343  axlowdim  29348  isgrpoi  30887  sspval  31112  0ofval  31176  ajfval  31198  hvmulex  31400  padct  33100  gsumwrd2dccat  33429  inftmrel  33531  isinftm  33532  smatrcl  34217  tpr2rico  34333  faeval  34668  mbfmco2  34687  br2base  34691  sxbrsigalem0  34693  sxbrsigalem3  34694  dya2iocrfn  34701  dya2iocct  34702  dya2iocnrect  34703  dya2iocuni  34705  dya2iocucvr  34706  sxbrsigalem2  34708  eulerpartlemgs2  34802  ccatmulgnn0dir  34964  afsval  35093  cvmlift2lem9  35824  satfv0  35871  satf00  35887  prv1n  35944  mexval  36015  mdvval  36017  mpstval  36048  brimg  36448  brrestrict  36462  colinearex  36573  nmulprop  36703  poimirlem4  38316  poimirlem28  38340  mblfinlem1  38349  heiborlem3  38505  rrnval  38519  ismrer1  38530  dfcnvrefrels2  39298  dfcnvrefrels3  39299  lcvfbr  39835  cmtfvalN  40025  cvrfval  40083  dvhvbase  41902  dvhfvadd  41906  dvhfvsca  41915  dibval  41957  dibfna  41969  dicval  41991  hdmap1fval  42611  ltex  43054  leex  43055  subex  43056  mzpincl  43506  pellexlem3  43599  pellexlem4  43600  pellexlem5  43601  aomclem6  43827  trclexi  44387  rtrclexi  44388  brtrclfv2  44494  mnringmulrcld  44993  hoiprodcl2  47310  hoicvrrex  47311  ovn0lem  47320  ovnhoilem1  47356  ovnlecvr2  47365  opnvonmbllem1  47387  opnvonmbllem2  47388  ovolval2lem  47398  ovolval2  47399  ovolval3  47402  ovolval4lem2  47405  ovolval5lem2  47408  ovnovollem1  47411  ovnovollem2  47412  smflimlem6  47531  gpgvtx  48849  gpgiedg  48850  sectfn  49848  nelsubc3  49890  cofidvala  49935  cofidval  49938  diag1f1lem  50125  fucoelvv  50139  fucofvalne  50144  functhinclem1  50263  functhinclem3  50265  functermc2  50328  idfudiag1bas  50343  idfudiag1  50344  prstchomval  50378  elpglem3  50532  pgindnf  50535  aacllem  50662