Theorem euim

Add unique existential quantifiers to an implication. Note the reversed implication in the antecedent. (Contributed by NM, 19-Oct-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Proof shortened by Wolf Lammen, 1-Oct-2023.)

Conclusion
\( \vdash \exists x \, \varphi \wedge \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists{!} x \, \psi \rightarrow \exists{!} x \, \varphi \)
Proof
l0
euimmo
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists{!} x \, \psi \rightarrow \exists^\ast x \, \varphi \)
exmoeub
biimpd _
\( \vdash \exists x \, \varphi \rightarrow \exists^\ast x \, \varphi \rightarrow \exists{!} x \, \varphi \)
sylan9r l0 _