Theorem eumo 2606

Description: Existential uniqueness implies uniqueness. (Contributed by NM, 23-Mar-1995.)

Assertion

Ref	Expression
eumo	⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

Proof of Theorem eumo

Step	Hyp	Ref	Expression
1		df-eu 2597	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2	1	simprbi 503	1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  ∃*wmo 2565  ∃!weu 2596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2597

This theorem is used by:  eumoi  2607  euimmo  2644  moaneu  2651  2exeuv  2660  eupick  2661  2eumo  2670  2exeu  2674  2eu2  2680  2eu5  2683  moeq3  3673  zfrep6  5246  euabex  5434  nfunsn  6953  dff3  7130  fnoprabg  7572  zfrep6OLD  7999  nqerf  11052  f1otrspeq  19703  uptx  23988  txcn  23989  omeueq  35830  bj-rep  38252  pm14.12  45659  euendfunc  50986  arweuthinc  50989  arweutermc  50990  mndtcobeq  51046