This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem spcegv

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 25-Aug-2023)

Ref Expression
Hypothesis spcgv.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion spcegv 
|- ( A e. V -> ( ps -> E. x ph ) )

Proof

Step Hyp Ref Expression
1 spcgv.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 elisset 
 |-  ( A e. V -> E. x x = A )
3 1 biimprcd 
 |-  ( ps -> ( x = A -> ph ) )
4 3 eximdv 
 |-  ( ps -> ( E. x x = A -> E. x ph ) )
5 2 4 syl5com 
 |-  ( A e. V -> ( ps -> E. x ph ) )