Theorem rspcimdv

Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rspcimdv.1	$$⊢\phi \to A\in B$$
2		rspcimdv.2	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \to \chi \right)$$
3		df-ral	$$⊢\forall x\in B\psi \leftrightarrow \forall x\left(x\in B\to \psi \right)$$
4		simpr	$$⊢\left(\phi \wedge x=A\right)\to x=A$$
5	4	eleq1d	$$⊢\left(\phi \wedge x=A\right)\to \left(x\in B\leftrightarrow A\in B\right)$$
6	5	biimprd	$$⊢\left(\phi \wedge x=A\right)\to \left(A\in B\to x\in B\right)$$
7	6 2	imim12d	$$⊢\left(\phi \wedge x=A\right)\to \left(\left(x\in B\to \psi \right)\to \left(A\in B\to \chi \right)\right)$$
8	1 7	spcimdv	$$⊢\phi \to \left(\forall x\left(x\in B\to \psi \right)\to \left(A\in B\to \chi \right)\right)$$
9	1 8	mpid	$$⊢\phi \to \left(\forall x\left(x\in B\to \psi \right)\to \chi \right)$$
10	3 9	biimtrid	$$⊢\phi \to \left(\forall x\in B\psi \to \chi \right)$$