Theorem rsp

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996)

	Ref	Expression
Assertion	rsp	|- ( A. x e. A ph -> ( x e. A -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp	|- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1 2	sylbi	|- ( A. x e. A ph -> ( x e. A -> ph ) )