Theorem spcimdv

Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		spcimdv.1	$$⊢\phi \to A\in B$$
2		spcimdv.2	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \to \chi \right)$$
3		elisset	$$⊢A\in B\to \exists xx=A$$
4	1 3	syl	$$⊢\phi \to \exists xx=A$$
5	2	ex	$$⊢\phi \to \left(x=A\to \left(\psi \to \chi \right)\right)$$
6	5	eximdv	$$⊢\phi \to \left(\exists xx=A\to \exists x\left(\psi \to \chi \right)\right)$$
7	4 6	mpd	$$⊢\phi \to \exists x\left(\psi \to \chi \right)$$
8		19.36v	$$⊢\exists x\left(\psi \to \chi \right)\leftrightarrow \left(\forall x\psi \to \chi \right)$$
9	7 8	sylib	$$⊢\phi \to \left(\forall x\psi \to \chi \right)$$