Theorem spcedv 3599

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

Step	Hyp	Ref	Expression
1		spcedv.1	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
2		spcedv.2	. 2 ⊢ (𝜑 → 𝜒)
3		spcedv.3	. . 3 ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))
4	3	spcegv 3597	. 2 ⊢ (𝑋 ∈ V → (𝜒 → ∃𝑥𝜓))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  zfrep6  7656  wfrlem15  7969  ertr  8304  f1dom2g  8527  dom3d  8551  disjenex  8675  domssex2  8677  domssex  8678  brwdom2  9037  infxpenc2lem2  9446  dfac8clem  9458  ac5num  9462  acni2  9472  acnlem  9474  finnisoeu  9539  infpss  9639  cofsmo  9691  axdc4lem  9877  ac6num  9901  axdclem2  9942  hasheqf1od  13715  fz1isolem  13820  wrd2f1tovbij  14324  fsum  15077  ntrivcvgn0  15254  fprod  15295  setsexstruct2  16522  isacs1i  16928  mreacs  16929  gsumval3lem2  19026  eltg3  21570  elptr  22181  nbusgrf1o1  27152  cusgrexg  27226  cusgrfilem3  27239  sizusglecusg  27245  wwlksnextbij  27680  eqvreltr  35857  clrellem  40031  clcnvlem  40032  fundcmpsurinj  43618  prproropen  43719  isomgreqve  44039  isomushgr  44040  isomgrsym  44050  isomgrtr  44053  ushrisomgr  44055  uspgrsprfo  44072  uspgrbispr  44075