Theorem dfmo 2565

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

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

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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  nexmo  2566  moim  2569  nfmo1  2582  nfmod2  2583  nfmodv  2584  mof  2588  mo3  2589  mo4  2591  eu3v  2595  cbvmovw  2627  cbvmow  2628  sbmo  2639  mopick  2650  2mo2  2672  rmoeq1  3396  mo2icl  3672  rmoanim  3842  axrep6  5241  axrep6OLD  5242  moabex  5433  moabexOLD  5434  dffun3  6545  dffun6f  6548  grothprim  10843  cbvmodavw  36870  mobidvALT  37600  wl-cbvmotv  38276  wl-moteq  38277  wl-moae  38279  wl-mo2df  38333  wl-mo2t  38338  wl-mo3t  38339  sn-axrep5v  43087  sn-axprlem3  43088  dffrege115  44818  mof0  49766