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