Theorem dfmo 2567

Description: Simplify definition df-mo 2566 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 2565	. 2 ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
2	1	df-mo 2566	1 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1558  ∃wex 1799  ∃*wmo 2564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-mo 2566

This theorem is referenced by:  nexmo  2568  moim  2571  nfmo1  2584  nfmod2  2585  nfmodv  2586  mof  2590  mo3  2591  mo4  2593  eu3v  2597  cbvmovw  2629  cbvmow  2630  sbmo  2641  mopick  2652  2mo2  2674  rmoeq1  3398  mo2icl  3677  rmoanim  3847  axrep6  5236  axrep6OLD  5237  moabex  5425  moabexOLD  5426  dffun3  6533  dffun6f  6536  grothprim  10792  cbvmodavw  36607  mobidvALT  37339  wl-cbvmotv  38013  wl-moteq  38014  wl-moae  38016  wl-mo2df  38070  wl-mo2t  38075  wl-mo3t  38076  sn-axrep5v  42833  sn-axprlem3  42834  dffrege115  44551  mof0  49456