Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020)
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 ) |
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 ) |