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 1540  ∃wex 1781  ∃*wmo 2537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  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  3373  mo2icl  3660  rmoanim  3832  axrep6  5221  axrep6OLD  5222  moabex  5410  moabexOLD  5411  dffun3  6510  dffun6f  6513  grothprim  10757  cbvmodavw  36432  mobidvALT  37164  wl-cbvmotv  37838  wl-moteq  37839  wl-moae  37841  wl-mo2df  37895  wl-mo2t  37900  wl-mo3t  37901  sn-axrep5v  42658  sn-axprlem3  42659  dffrege115  44405  mof0  49313