Theorem dfmo 2568

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

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem dfmo

Dummy variable 𝑧 is distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1809  ∃*wmo 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567

This theorem is referenced by:  nexmo  2569  moim  2572  nfmo1  2585  nfmod2  2586  nfmodv  2587  mof  2591  mo3  2592  mo4  2594  eu3v  2598  cbvmovw  2630  cbvmow  2631  sbmo  2642  mopick  2653  2mo2  2675  rmoeq1  3400  mo2icl  3677  rmoanim  3848  axrep6  5247  axrep6OLD  5248  moabex  5439  moabexOLD  5440  dffun3  6548  dffun6f  6551  grothprim  10814  cbvmodavw  36762  mobidvALT  37492  wl-cbvmotv  38168  wl-moteq  38169  wl-moae  38171  wl-mo2df  38225  wl-mo2t  38230  wl-mo3t  38231  sn-axrep5v  42988  sn-axprlem3  42989  dffrege115  44704  mof0  49616