Metamath Proof Explorer

Theorem dfmo

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

Ref Expression
Assertion dfmo 
|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )

Proof

Step Hyp Ref Expression
1 mojust 
 |-  ( E. y A. x ( ph -> x = y ) <-> E. z A. x ( ph -> x = z ) )
2 1 df-mo 
 |-  ( E* x ph <-> E. y A. x ( ph -> x = y ) )