Description: Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997)
Ref | Expression | ||
---|---|---|---|
Hypotheses | spcgf.1 | |- F/_ x A |
|
spcgf.2 | |- F/ x ps |
||
spcgf.3 | |- ( x = A -> ( ph <-> ps ) ) |
||
Assertion | spcegf | |- ( A e. V -> ( ps -> E. x ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcgf.1 | |- F/_ x A |
|
2 | spcgf.2 | |- F/ x ps |
|
3 | spcgf.3 | |- ( x = A -> ( ph <-> ps ) ) |
|
4 | 2 | nfn | |- F/ x -. ps |
5 | 3 | notbid | |- ( x = A -> ( -. ph <-> -. ps ) ) |
6 | 1 4 5 | spcgf | |- ( A e. V -> ( A. x -. ph -> -. ps ) ) |
7 | 6 | con2d | |- ( A e. V -> ( ps -> -. A. x -. ph ) ) |
8 | df-ex | |- ( E. x ph <-> -. A. x -. ph ) |
|
9 | 7 8 | syl6ibr | |- ( A e. V -> ( ps -> E. x ph ) ) |