Theorem dfmo 2544

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545  ∃wex 1786  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543

This theorem is referenced by:  nexmo  2545  moim  2548  nfmo1  2561  nfmod2  2562  nfmodv  2563  mof  2567  mo3  2568  mo4  2570  eu3v  2574  cbvmovw  2606  cbvmow  2607  sbmo  2618  mopick  2629  2mo2  2651  rmoeq1  3375  mo2icl  3655  rmoanim  3826  axrep6  5208  axrep6OLD  5209  moabex  5397  moabexOLD  5398  dffun3  6497  dffun6f  6500  grothprim  10748  cbvmodavw  36478  mobidvALT  37210  wl-cbvmotv  37884  wl-moteq  37885  wl-moae  37887  wl-mo2df  37941  wl-mo2t  37946  wl-mo3t  37947  sn-axrep5v  42704  sn-axprlem3  42705  dffrege115  44422  mof0  49328