Metamath Proof Explorer


Theorem spcedv

Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020)

Ref Expression
Hypotheses spcedv.1 ( 𝜑𝑋 ∈ V )
spcedv.2 ( 𝜑𝜒 )
spcedv.3 ( 𝑥 = 𝑋 → ( 𝜓𝜒 ) )
Assertion spcedv ( 𝜑 → ∃ 𝑥 𝜓 )

Proof

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