Theorem exmoeu

Existence is equivalent to uniqueness implying existential uniqueness. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Wolf Lammen, 5-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.)

Conclusion
\( \vdash \exists x \, \varphi \leftrightarrow \exists^\ast x \, \varphi \rightarrow \exists{!} x \, \varphi \)
Proof
exmoeub
l1
biimpd _
nexmo
l3
con1i _
euex
ja l3 _
impbii l1 _