Theorem dfmo 2540

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780  ∃*wmo 2537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539

This theorem is referenced by:  nexmo  2541  moim  2544  nfmo1  2557  nfmod2  2558  nfmodv  2559  mof  2563  mo3  2564  mo4  2566  eu3v  2570  cbvmovw  2602  cbvmow  2603  sbmo  2614  mopick  2625  2mo2  2647  rmoeq1  3381  mo2icl  3672  rmoanim  3844  axrep6  5233  axrep6OLD  5234  moabex  5406  moabexOLD  5407  dffun3  6504  dffun6f  6507  grothprim  10745  cbvmodavw  36444  mobidvALT  37058  wl-cbvmotv  37718  wl-moteq  37719  wl-moae  37721  wl-mo2df  37775  wl-mo2t  37780  wl-mo3t  37781  sn-axrep5v  42473  sn-axprlem3  42474  dffrege115  44219  mof0  49083