# Metamath Proof Explorer

## 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 less 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 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
spime.2 ${⊢}{x}={y}\to \left({\phi }\to {\psi }\right)$
Assertion spime ${⊢}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

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