Theorem spcdv

Description: Rule of specialization, using implicit substitution. Analogous to rspcdv . (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		spcimdv.1	$$⊢\phi \to A\in B$$
2		spcdv.2	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \leftrightarrow \chi \right)$$
3	2	biimpd	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \to \chi \right)$$
4	1 3	spcimdv	$$⊢\phi \to \left(\forall x\psi \to \chi \right)$$