Metamath Proof Explorer


Theorem spcedv

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

Ref Expression
Hypotheses spcedv.1 φ X V
spcedv.2 φ χ
spcedv.3 x = X ψ χ
Assertion spcedv φ x ψ

Proof

Step Hyp Ref Expression
1 spcedv.1 φ X V
2 spcedv.2 φ χ
3 spcedv.3 x = X ψ χ
4 3 spcegv X V χ x ψ
5 1 2 4 sylc φ x ψ