This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to \forall x φ$
	spimew.2	$⊢ x = y \to (φ \to ψ)$
Assertion	spimew	$⊢ φ \to \exists x ψ$

Proof

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