Theorem spime

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

	Ref	Expression
Hypotheses	spime.1	|- F/ x ph
	spime.2	|- ( x = y -> ( ph -> ps ) )
Assertion	spime	|- ( ph -> E. x ps )

Proof

Step	Hyp	Ref	Expression
1		spime.1	|- F/ x ph
2		spime.2	|- ( x = y -> ( ph -> ps ) )
3	1	a1i	|- ( T. -> F/ x ph )
4	3 2	spimed	|- ( T. -> ( ph -> E. x ps ) )
5	4	mptru	|- ( ph -> E. x ps )