Theorem spcgv

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of Quine p. 44. (Contributed by NM, 22-Jun-1994) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 25-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		spcgv.1	|- ( x = A -> ( ph <-> ps ) )
2		elex	|- ( A e. V -> A e. _V )
3		id	|- ( A e. _V -> A e. _V )
4	1	adantl	|- ( ( A e. _V /\ x = A ) -> ( ph <-> ps ) )
5	3 4	spcdv	|- ( A e. _V -> ( A. x ph -> ps ) )
6	2 5	syl	|- ( A e. V -> ( A. x ph -> ps ) )