Theorem rspa

Description: Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		rsp	$$⊢\forall x\in A\phi \to \left(x\in A\to \phi \right)$$
2	1	imp	$$⊢\left(\forall x\in A\phi \wedge x\in A\right)\to \phi$$