Metamath Proof Explorer


Theorem spcegf

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 ) )

Proof

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 ) )