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

Theorem xpexd 7690
Description: The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
xpexd.1 (𝜑𝐴𝑉)
xpexd.2 (𝜑𝐵𝑊)
Assertion
Ref Expression
xpexd (𝜑 → (𝐴 × 𝐵) ∈ V)

Proof of Theorem xpexd
StepHypRef Expression
1 xpexd.1 . 2 (𝜑𝐴𝑉)
2 xpexd.2 . 2 (𝜑𝐵𝑊)
3 xpexg 7689 . 2 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴 × 𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3448   × cxp 5636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-opab 5173  df-xp 5644  df-rel 5645
This theorem is referenced by:  cnvexg  7866  cofunexg  7886  oprabexd  7913  ofmresex  7923  opabex2  7994  offval22  8025  sexp2  8083  sexp3  8090  tposexg  8176  mapunen  9097  marypha1  9377  wdom2d  9523  ixpiunwdom  9533  ttrclexg  9666  fnct  10480  fpwwe2lem2  10575  fpwwe2lem4  10577  fpwwe2lem11  10584  fpwwelem  10588  canthwe  10594  pwxpndom  10609  gchhar  10622  trclexlem  14886  isacs1i  17544  brcic  17688  rescval2  17718  reschom  17721  rescabs  17725  rescabsOLD  17726  setccofval  17975  estrccofval  18023  sylow2a  19408  gsumxp  19760  gsumxp2  19764  opsrval  21463  opsrtoslem2  21479  evlslem4  21500  matbas2d  21788  tsmsxp  23522  ustssel  23573  ustfilxp  23580  trust  23597  restutop  23605  trcfilu  23662  cfiluweak  23663  imasdsf1olem  23742  metustfbas  23929  restmetu  23942  rrxsca  24776  madeval  27204  perpln1  27694  perpln2  27695  isperp  27696  suppovss  31640  fsuppcurry1  31684  fsuppcurry2  31685  hashxpe  31751  gsumpart  31939  fedgmullem1  32364  fedgmullem2  32365  fedgmul  32366  metidval  32511  esumiun  32733  filnetlem3  34881  bj-imdirvallem  35680  bj-imdirval2  35683  bj-imdirco  35690  bj-iminvval2  35694  isrngod  36386  isgrpda  36443  iscringd  36486  evlsbagval  40777  evlsevl  40781  wdom2d2  41388  unxpwdom3  41451  trclubgNEW  41964  relexpxpmin  42063  rfovd  42347  rfovcnvf1od  42350  fsovrfovd  42355  dvsinax  44228  sge0xp  44744
  Copyright terms: Public domain W3C validator