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 1567  ∃wex 1811  ∃*wmo 2562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  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  3671  rmoanim  3842  axrep6  5239  moabex  5425  moabexOLD  5426  dffun3  6553  dffun6f  6556  grothprim  10924  cbvmodavw  37133  mobidvALT  37863  wl-cbvmotv  38552  wl-moteq  38553  wl-moae  38555  wl-mo2df  38609  wl-mo2t  38614  wl-mo3t  38615  sn-axrep5v  43378  sn-axprlem3  43379  dffrege115  45085  mof0  50056