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  3383  mo2icl  3674  rmoanim  3846  axrep6  5235  axrep6OLD  5236  moabex  5413  moabexOLD  5414  dffun3  6512  dffun6f  6515  grothprim  10757  cbvmodavw  36466  mobidvALT  37105  wl-cbvmotv  37768  wl-moteq  37769  wl-moae  37771  wl-mo2df  37825  wl-mo2t  37830  wl-mo3t  37831  sn-axrep5v  42589  sn-axprlem3  42590  dffrege115  44334  mof0  49197