Theorem 19.8a

If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. See 19.8v for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)

Conclusion
\( \vdash \varphi \rightarrow \exists x \, \varphi \)
Proof
l0
ax12v
\( \vdash x = y \rightarrow \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
alequexv
\( \vdash \forall x \, (x = y \rightarrow \varphi) \rightarrow \exists x \, \varphi \)
l2
syl6 l0 _
\( \vdash x = y \rightarrow \varphi \rightarrow \exists x \, \varphi \)
ax6evr
\( \vdash \exists y \, x = y \)
exlimiiv l2 _