Theorem euimmo

Existential uniqueness implies uniqueness through reverse implication. (Contributed by NM, 22-Apr-1995.)

Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists{!} x \, \psi \rightarrow \exists^\ast x \, \varphi \)
Proof
l0
eumo
\( \vdash \exists{!} x \, \psi \rightarrow \exists^\ast x \, \psi \)
moim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists^\ast x \, \psi \rightarrow \exists^\ast x \, \varphi \)
syl5 l0 _