Theorem eumo 2638

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

Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2596  ∃!weu 2628

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 2629

This theorem is referenced by:  eumoi  2639  euimmo  2677  moaneu  2685  2exeuv  2694  eupick  2695  2eumo  2704  2exeu  2708  2eu2  2714  2eu5  2717  2eu5OLD  2718  moeq3  3651  euabex  5318  nfunsn  6682  dff3  6843  fnoprabg  7254  zfrep6  7638  nqerf  10341  f1otrspeq  18567  uptx  22230  txcn  22231  pm14.12  41125