Theorem nexmo

Nonexistence implies uniqueness. (Contributed by BJ, 30-Sep-2022.) Avoid [ax-11]. (Revised by Wolf Lammen, 16-Oct-2022.)

Conclusion
\( \vdash \neg \exists x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
Proof
pm2.21
alimi _
alrimiv _
l3
19.2d _
\( \vdash \forall x \, \neg \varphi \rightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
alnex
l5
bicomi _
\( \vdash \neg \exists x \, \varphi \leftrightarrow \forall x \, \neg \varphi \)
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
3imtr4i l3 l5 _