MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpex Structured version   Visualization version   GIF version

Theorem xpex 7465
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
StepHypRef Expression
1 xpex.1 . 2 𝐴 ∈ V
2 xpex.2 . 2 𝐵 ∈ V
3 xpexg 7462 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 × 𝐵) ∈ V)
41, 2, 3mp2an 688 1 (𝐴 × 𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3492   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-opab 5120  df-xp 5554  df-rel 5555
This theorem is referenced by:  oprabex  7666  oprabex3  7667  mpoexw  7765  fnpm  8403  mapsnf1o2  8446  ixpsnf1o  8490  xpsnen  8589  endisj  8592  xpcomen  8596  xpassen  8599  xpmapenlem  8672  mapunen  8674  unxpdomlem3  8712  hartogslem1  8994  rankxpl  9292  rankfu  9294  rankmapu  9295  rankxplim  9296  rankxplim2  9297  rankxplim3  9298  rankxpsuc  9299  r0weon  9426  infxpenlem  9427  infxpenc2lem2  9434  dfac3  9535  dfac5lem2  9538  dfac5lem3  9539  dfac5lem4  9540  unctb  9615  axcc2lem  9846  axdc3lem  9860  axdc4lem  9865  enqex  10332  nqex  10333  nrex1  10474  enrex  10477  axcnex  10557  zexALT  11989  cnexALT  12373  addex  12375  mulex  12376  ixxex  12737  shftfval  14417  climconst2  14893  cpnnen  15570  ruclem13  15583  cnso  15588  prdsval  16716  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  prdsle  16723  prdsds  16725  prdshom  16728  prdsco  16729  fnmrc  16866  mrcfval  16867  mreacs  16917  comfffval  16956  oppccofval  16974  sectfval  17009  brssc  17072  sscpwex  17073  isssc  17078  isfunc  17122  isfuncd  17123  idfu2nd  17135  idfu1st  17137  idfucl  17139  wunfunc  17157  fuccofval  17217  homafval  17277  homaf  17278  homaval  17279  coapm  17319  catccofval  17348  catcfuccl  17357  xpcval  17415  xpcbas  17416  xpchom  17418  xpccofval  17420  1stfval  17429  2ndfval  17432  1stfcl  17435  2ndfcl  17436  catcxpccl  17445  evlf2  17456  evlf1  17458  evlfcl  17460  hof1fval  17491  hof2fval  17493  hofcl  17497  ipoval  17752  letsr  17825  frmdplusg  18007  eqgfval  18266  efglem  18771  efgval  18772  psrplusg  20089  ltbval  20180  opsrle  20184  evlslem2  20220  evlssca  20230  mpfind  20248  evls1sca  20414  pf1ind  20446  cnfldds  20483  cnfldfun  20485  cnfldfunALT  20486  xrsadd  20490  xrsmul  20491  xrsle  20493  xrsds  20516  znle  20611  pjfval  20778  mat1dimmul  21013  2ndcctbss  21991  txuni2  22101  txbas  22103  eltx  22104  txcnp  22156  txcnmpt  22160  txrest  22167  txlm  22184  tx1stc  22186  tx2ndc  22187  txkgen  22188  txflf  22542  cnextfval  22598  distgp  22635  indistgp  22636  ustfn  22737  ustn0  22756  ussid  22796  ressuss  22799  ishtpy  23503  isphtpc  23525  elovolmlem  24002  dyadmbl  24128  vitali  24141  mbfimaopnlem  24183  dvfval  24422  plyeq0lem  24727  taylfval  24874  ulmval  24895  dmarea  25462  dchrplusg  25750  tgjustc1  26188  tgjustc2  26189  iscgrg  26225  ishlg  26315  ishpg  26472  iscgra  26522  isinag  26551  isleag  26560  axlowdimlem15  26669  axlowdim  26674  isgrpoi  28202  sspval  28427  0ofval  28491  ajfval  28513  hvmulex  28715  inftmrel  30736  isinftm  30737  smatrcl  30960  tpr2rico  31054  faeval  31404  mbfmco2  31422  br2base  31426  sxbrsigalem0  31428  sxbrsigalem3  31429  dya2iocrfn  31436  dya2iocct  31437  dya2iocnrect  31438  dya2iocuni  31440  dya2iocucvr  31441  sxbrsigalem2  31443  eulerpartlemgs2  31537  ccatmulgnn0dir  31711  afsval  31841  cvmlift2lem9  32455  satfv0  32502  satf00  32518  prv1n  32575  mexval  32646  mdvval  32648  mpstval  32679  brimg  33295  brrestrict  33307  colinearex  33418  poimirlem4  34777  poimirlem28  34801  mblfinlem1  34810  heiborlem3  34972  rrnval  34986  ismrer1  34997  dfcnvrefrels2  35646  dfcnvrefrels3  35647  lcvfbr  36036  cmtfvalN  36226  cvrfval  36284  dvhvbase  38103  dvhfvadd  38107  dvhfvsca  38116  dibval  38158  dibfna  38170  dicval  38192  hdmap1fval  38812  mzpincl  39209  pellexlem3  39306  pellexlem4  39307  pellexlem5  39308  aomclem6  39537  trclexi  39858  rtrclexi  39859  brtrclfv2  39950  hoiprodcl2  42714  hoicvrrex  42715  ovn0lem  42724  ovnhoilem1  42760  ovnlecvr2  42769  opnvonmbllem1  42791  opnvonmbllem2  42792  ovolval2lem  42802  ovolval2  42803  ovolval3  42806  ovolval4lem2  42809  ovolval5lem2  42812  ovnovollem1  42815  ovnovollem2  42816  smflimlem6  42929  elpglem3  44743  aacllem  44830
  Copyright terms: Public domain W3C validator