Theorem rsp

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

	Ref	Expression
Assertion	rsp	$$⊢\forall x\in A\phi \to \left(x\in A\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
2		sp	$$⊢\forall x\left(x\in A\to \phi \right)\to \left(x\in A\to \phi \right)$$
3	1 2	sylbi	$$⊢\forall x\in A\phi \to \left(x\in A\to \phi \right)$$