Theorem rspccva

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Hypothesis	rspcv.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	rspccva	|- ( ( A. x e. B ph /\ A e. B ) -> 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	impcom	|- ( ( A. x e. B ph /\ A e. B ) -> ps )