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

Theorem xpexd 7463
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 7462 . 2 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 × 𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  cnvexg  7618  cofunexg  7639  oprabexd  7665  ofmresex  7675  opabex2  7744  offval22  7772  tposexg  7895  marypha1  8886  wdom2d  9032  ixpiunwdom  9043  fnct  9947  fpwwe2lem2  10042  fpwwe2lem5  10044  fpwwe2lem12  10051  fpwwelem  10055  canthwe  10061  pwxpndom  10076  gchhar  10089  trclexlem  14342  isacs1i  16916  brcic  17056  rescval2  17086  reschom  17088  rescabs  17091  setccofval  17330  estrccofval  17367  sylow2a  18673  lsmhash  18760  gsumxp  19025  gsumxp2  19029  opsrval  20183  opsrtoslem2  20193  evlslem4  20216  matbas2d  20960  tsmsxp  22690  ustssel  22741  ustfilxp  22748  trust  22765  restutop  22773  trcfilu  22830  cfiluweak  22831  imasdsf1olem  22910  metustfbas  23094  restmetu  23107  rrxsca  23926  perpln1  26423  perpln2  26424  isperp  26425  suppovss  30354  fsuppcurry1  30387  fsuppcurry2  30388  hashxpe  30455  fedgmullem1  30924  fedgmullem2  30925  fedgmul  30926  metidval  31029  esumiun  31252  madeval  33186  filnetlem3  33625  bj-imdirval  34364  bj-imdirval2  34365  isrngod  35057  isgrpda  35114  iscringd  35157  wdom2d2  39510  unxpwdom3  39573  trclubgNEW  39856  relexpxpmin  39940  rfovd  40225  rfovcnvf1od  40228  fsovrfovd  40233  dvsinax  42073  sge0xp  42588
  Copyright terms: Public domain W3C validator