Theorem dfmo 2541

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃wex 1781  ∃*wmo 2538

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 2540

This theorem is referenced by:  nexmo  2542  moim  2545  nfmo1  2558  nfmod2  2559  nfmodv  2560  mof  2564  mo3  2565  mo4  2567  eu3v  2571  cbvmovw  2603  cbvmow  2604  sbmo  2615  mopick  2626  2mo2  2648  rmoeq1  3374  mo2icl  3661  rmoanim  3833  axrep6  5221  axrep6OLD  5222  moabex  5405  moabexOLD  5406  dffun3  6504  dffun6f  6507  grothprim  10748  cbvmodavw  36448  mobidvALT  37180  wl-cbvmotv  37852  wl-moteq  37853  wl-moae  37855  wl-mo2df  37909  wl-mo2t  37914  wl-mo3t  37915  sn-axrep5v  42672  sn-axprlem3  42673  dffrege115  44423  mof0  49325