Theorem rspcdf

Description: Restricted specialization, using implicit substitution. (Contributed by Emmett Weisz, 16-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rspcdf.1	$$⊢Ⅎx\phi$$
2		rspcdf.2	$$⊢Ⅎx\chi$$
3		rspcdf.3	$$⊢\phi \to A\in B$$
4		rspcdf.4	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \leftrightarrow \chi \right)$$
5	4	ex	$$⊢\phi \to \left(x=A\to \left(\psi \leftrightarrow \chi \right)\right)$$
6	1 5	alrimi	$$⊢\phi \to \forall x\left(x=A\to \left(\psi \leftrightarrow \chi \right)\right)$$
7	2	rspct	$$⊢\forall x\left(x=A\to \left(\psi \leftrightarrow \chi \right)\right)\to \left(A\in B\to \left(\forall x\in B\psi \to \chi \right)\right)$$
8	6 3 7	sylc	$$⊢\phi \to \left(\forall x\in B\psi \to \chi \right)$$