Theorem dfmo 2570

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

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

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 2569

This theorem is used by:  nexmo  2571  moim  2574  nfmo1  2587  nfmod2  2588  nfmodv  2589  mof  2593  mo3  2594  mo4  2596  eu3v  2600  cbvmovw  2632  cbvmow  2633  sbmo  2644  mopick  2655  2mo2  2677  rmoeq1  3402  mo2icl  3679  rmoanim  3849  axrep6  5249  axrep6OLD  5250  moabex  5441  moabexOLD  5442  dffun3  6552  dffun6f  6555  grothprim  10834  cbvmodavw  36819  mobidvALT  37549  wl-cbvmotv  38225  wl-moteq  38226  wl-moae  38228  wl-mo2df  38282  wl-mo2t  38287  wl-mo3t  38288  sn-axrep5v  43046  sn-axprlem3  43047  dffrege115  44762  mof0  49673