Theorem dfmo 2566

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

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

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 2565

This theorem is used by:  nexmo  2567  moim  2570  nfmo1  2583  nfmod2  2584  nfmodv  2585  mof  2589  mo3  2590  mo4  2592  eu3v  2596  cbvmovw  2628  cbvmow  2629  sbmo  2640  mopick  2651  2mo2  2673  rmoeq1  3397  mo2icl  3672  rmoanim  3842  axrep6  5240  moabex  5426  moabexOLD  5427  dffun3  6549  dffun6f  6552  grothprim  10912  cbvmodavw  37019  mobidvALT  37749  wl-cbvmotv  38425  wl-moteq  38426  wl-moae  38428  wl-mo2df  38482  wl-mo2t  38487  wl-mo3t  38488  sn-axrep5v  43251  sn-axprlem3  43252  dffrege115  44963  mof0  49917