Theorem dfmo 2574

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565  ∃wex 1806  ∃*wmo 2571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573

This theorem is referenced by:  nexmo  2575  moim  2578  nfmo1  2591  nfmod2  2592  nfmodv  2593  mof  2597  mo3  2598  mo4  2600  eu3v  2604  cbvmovw  2636  cbvmow  2637  sbmo  2648  mopick  2659  2mo2  2681  rmoeq1  3407  mo2icl  3686  rmoanim  3856  axrep6  5251  axrep6OLD  5252  moabex  5440  moabexOLD  5441  dffun3  6549  dffun6f  6552  grothprim  10818  cbvmodavw  36650  mobidvALT  37380  wl-cbvmotv  38055  wl-moteq  38056  wl-moae  38058  wl-mo2df  38112  wl-mo2t  38117  wl-mo3t  38118  sn-axrep5v  42877  sn-axprlem3  42878  dffrege115  44595  mof0  49500