Theorem rspcva

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005)

	Ref	Expression
Hypothesis	rspcv.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	rspcva	|- ( ( A e. B /\ A. x e. B ph ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		rspcv.1	|- ( x = A -> ( ph <-> ps ) )
2	1	rspcv	|- ( A e. B -> ( A. x e. B ph -> ps ) )
3	2	imp	|- ( ( A e. B /\ A. x e. B ph ) -> ps )