Theorem dfmo

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

	Ref	Expression
Assertion	dfmo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mojust	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \exists z\forall x\left(\phi \to x=z\right)$$
2	1	df-mo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$