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

Theorem spcedv 3584
 Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.)
Hypotheses
Ref Expression
spcedv.1 (𝜑𝑋 ∈ V)
spcedv.2 (𝜑𝜒)
spcedv.3 (𝑥 = 𝑋 → (𝜓𝜒))
Assertion
Ref Expression
spcedv (𝜑 → ∃𝑥𝜓)
Distinct variable groups:   𝑥,𝑋   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem spcedv
StepHypRef Expression
1 spcedv.1 . 2 (𝜑𝑋 ∈ V)
2 spcedv.2 . 2 (𝜑𝜒)
3 spcedv.3 . . 3 (𝑥 = 𝑋 → (𝜓𝜒))
43spcegv 3582 . 2 (𝑋 ∈ V → (𝜒 → ∃𝑥𝜓))
51, 2, 4sylc 65 1 (𝜑 → ∃𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2115  Vcvv 3479 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896 This theorem is referenced by:  zfrep6  7639  wfrlem15  7952  ertr  8287  f1dom2g  8510  dom3d  8534  disjenex  8659  domssex2  8661  domssex  8662  brwdom2  9021  infxpenc2lem2  9431  dfac8clem  9443  ac5num  9447  acni2  9457  acnlem  9459  finnisoeu  9524  infpss  9624  cofsmo  9676  axdc4lem  9862  ac6num  9886  axdclem2  9927  hasheqf1od  13708  fz1isolem  13813  wrd2f1tovbij  14313  fsum  15066  ntrivcvgn0  15243  fprod  15284  setsexstruct2  16511  isacs1i  16917  mreacs  16918  gsumval3lem2  19015  eltg3  21556  elptr  22167  nbusgrf1o1  27149  cusgrexg  27223  cusgrfilem3  27236  sizusglecusg  27242  wwlksnextbij  27677  bj-imdirco  34509  eqvreltr  35902  clrellem  40154  clcnvlem  40155  fundcmpsurinj  43768  prproropen  43867  isomgreqve  44185  isomushgr  44186  isomgrsym  44196  isomgrtr  44199  ushrisomgr  44201  uspgrsprfo  44218  uspgrbispr  44221  naryenef  44899
 Copyright terms: Public domain W3C validator