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  10819  cbvmodavw  36685  mobidvALT  37415  wl-cbvmotv  38090  wl-moteq  38091  wl-moae  38093  wl-mo2df  38147  wl-mo2t  38152  wl-mo3t  38153  sn-axrep5v  42912  sn-axprlem3  42913  dffrege115  44630  mof0  49535