Theorem rspc

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005) (Revised by Mario Carneiro, 11-Oct-2016)

	Ref	Expression
Hypotheses	rspc.1	$$⊢Ⅎx\psi$$
	rspc.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rspc	$$⊢A\in B\to \left(\forall x\in B\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rspc.1	$$⊢Ⅎx\psi$$
2		rspc.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3		df-ral	$$⊢\forall x\in B\phi \leftrightarrow \forall x\left(x\in B\to \phi \right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
5		nfv	$$⊢ℲxA\in B$$
6	5 1	nfim	$$⊢Ⅎx\left(A\in B\to \psi \right)$$
7		eleq1	$$⊢x=A\to \left(x\in B\leftrightarrow A\in B\right)$$
8	7 2	imbi12d	$$⊢x=A\to \left(\left(x\in B\to \phi \right)\leftrightarrow \left(A\in B\to \psi \right)\right)$$
9	4 6 8	spcgf	$$⊢A\in B\to \left(\forall x\left(x\in B\to \phi \right)\to \left(A\in B\to \psi \right)\right)$$
10	9	pm2.43a	$$⊢A\in B\to \left(\forall x\left(x\in B\to \phi \right)\to \psi \right)$$
11	3 10	syl5bi	$$⊢A\in B\to \left(\forall x\in B\phi \to \psi \right)$$