Theorem eumo 2573

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

Syntax hints:   → wi 4  ∃wex 1782  ∃*wmo 2533  ∃!weu 2563

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 206  df-an 398  df-eu 2564

This theorem is referenced by:  eumoi  2574  euimmo  2613  moaneu  2620  2exeuv  2629  eupick  2630  2eumo  2639  2exeu  2643  2eu2  2649  2eu5  2652  moeq3  3709  euabex  5462  nfunsn  6934  dff3  7102  fnoprabg  7531  zfrep6  7941  nqerf  10925  f1otrspeq  19315  uptx  23129  txcn  23130  pm14.12  43180  mndtcbas2  47709