Theorem spime

Description: Existential introduction, using implicit substitution. Compare Lemma 14 of Tarski p. 70. See spimew and spimevw for weaker versions requiring fewer axioms. (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 3-Oct-2016) (Proof shortened by Wolf Lammen, 6-Mar-2018) Usage of this theorem is discouraged because it depends on ax-13 . Use spimefv instead. (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		spime.1	$$⊢Ⅎx\phi$$
2		spime.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
3	1	a1i	$$⊢\top \to Ⅎx\phi$$
4	3 2	spimed	$$⊢\top \to \left(\phi \to \exists x\psi \right)$$
5	4	mptru	$$⊢\phi \to \exists x\psi$$