Theorem dfmo

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

	Ref	Expression
Assertion	dfmo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		mojust	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) )
2	1	df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )