Theorem dfmo 2568

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812  ∃*wmo 2565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567

This theorem is used by:  nexmo  2569  moim  2572  nfmo1  2585  nfmod2  2586  nfmodv  2587  mof  2591  mo3  2592  mo4  2594  eu3v  2598  cbvmovw  2630  cbvmow  2631  sbmo  2642  mopick  2653  2mo2  2675  rmoeq1  3400  mo2icl  3675  rmoanim  3846  axrep6  5246  moabex  5433  moabexOLD  5434  dffun3  6578  dffun6f  6581  grothprim  10958  elpssmo  36673  cbvmodavw  37254  mobidvALT  37984  wl-cbvmotv  38713  wl-moteq  38714  wl-moae  38716  wl-mo2df  38770  wl-mo2t  38775  wl-mo3t  38776  sn-axrep5v  43538  sn-axprlem3  43539  dffrege115  45239  mof0  50280