Theorem speimfw

Description: Specialization, with additional weakening (compared to 19.2 ) to allow bundling of x and y . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017) (Proof shortened by Wolf Lammen, 5-Dec-2017)

	Ref	Expression
Hypothesis	speimfw.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
Assertion	speimfw	$$⊢\neg \forall x\neg x=y\to \left(\forall x\phi \to \exists x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		speimfw.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
2		df-ex	$$⊢\exists xx=y\leftrightarrow \neg \forall x\neg x=y$$
3	2	biimpri	$$⊢\neg \forall x\neg x=y\to \exists xx=y$$
4	1	com12	$$⊢\phi \to \left(x=y\to \psi \right)$$
5	4	aleximi	$$⊢\forall x\phi \to \left(\exists xx=y\to \exists x\psi \right)$$
6	3 5	syl5com	$$⊢\neg \forall x\neg x=y\to \left(\forall x\phi \to \exists x\psi \right)$$