Theorem eupick

Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing \( x \) such that \( \varphi \) is true, and there is also an \( x \) (actually the same one) such that \( \varphi \) and \( \psi \) are both true, then \( \varphi \) implies \( \psi \) regardless of \( x \). This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by NM, 10-Jul-1994.)

Conclusion
\( \vdash \exists{!} x \, \varphi \wedge \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \rightarrow \psi \)
Proof
l0
eumo
\( \vdash \exists{!} x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
mopick
\( \vdash \exists^\ast x \, \varphi \wedge \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \rightarrow \psi \)
sylan l0 _