Theorem dfmo

Simplify definition [df-mo] by removing its provable hypothesis. (Contributed by Wolf Lammen, 15-Feb-2026.)

Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
Proof
mojust
\( \vdash \exists y \, \forall x \, (\varphi \rightarrow x = y) \leftrightarrow \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
df-mo _