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
|- ( ph -> X e. V )
spcedv.2
|- ( ph -> ch )
spcedv.3
|- ( x = X -> ( ps <-> ch ) )
Assertion spcedv
|- ( ph -> E. x ps )

Proof

Step Hyp Ref Expression
1 spcedv.1
 |-  ( ph -> X e. V )
2 spcedv.2
 |-  ( ph -> ch )
3 spcedv.3
 |-  ( x = X -> ( ps <-> ch ) )
4 3 spcegv
 |-  ( X e. V -> ( ch -> E. x ps ) )
5 1 2 4 sylc
 |-  ( ph -> E. x ps )