Theorem eumo 2580

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 2571	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2	1	simprbi 500	1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1786  ∃*wmo 2539  ∃!weu 2570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-eu 2571

This theorem is referenced by:  eumoi  2581  euimmo  2620  moaneu  2627  2exeuv  2636  eupick  2637  2eumo  2646  2exeu  2650  2eu2  2656  2eu5  2659  moeq3  3616  euabex  5329  nfunsn  6723  dff3  6888  fnoprabg  7301  zfrep6  7693  nqerf  10442  f1otrspeq  18705  uptx  22388  txcn  22389  pm14.12  41617