Theorem eumo 2582

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

Syntax hints:   → wi 4  ∃wex 1786  ∃*wmo 2541  ∃!weu 2572

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 208  df-an 397  df-eu 2573

This theorem is referenced by:  eumoi  2583  euimmo  2620  moaneu  2627  2exeuv  2636  eupick  2637  2eumo  2646  2exeu  2650  2eu2  2656  2eu5  2659  moeq3  3653  zfrep6  5211  euabex  5400  nfunsn  6866  dff3  7041  fnoprabg  7479  zfrep6OLD  7897  nqerf  10844  f1otrspeq  19413  uptx  23608  txcn  23609  bj-rep  37426  pm14.12  44865  euendfunc  50016  arweuthinc  50019  arweutermc  50020  mndtcbas2  50073