Theorem spimew

Description: Existential introduction, using implicit substitution. Compare Lemma 14 of Tarski p. 70. (Contributed by NM, 7-Aug-1994) (Proof shortened by Wolf Lammen, 22-Oct-2023)

	Ref	Expression
Hypotheses	spimew.1	$$⊢\phi \to \forall x\phi$$
	spimew.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
Assertion	spimew	$$⊢\phi \to \exists x\psi$$

Proof

Step	Hyp	Ref	Expression
1		spimew.1	$$⊢\phi \to \forall x\phi$$
2		spimew.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
3		ax6v	$$⊢\neg \forall x\neg x=y$$
4	2	speimfw	$$⊢\neg \forall x\neg x=y\to \left(\forall x\phi \to \exists x\psi \right)$$
5	3 1 4	mpsyl	$$⊢\phi \to \exists x\psi$$