Theorem eumo 2572

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

Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2532  ∃!weu 2562

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 397  df-eu 2563

This theorem is referenced by:  eumoi  2573  euimmo  2612  moaneu  2619  2exeuv  2628  eupick  2629  2eumo  2638  2exeu  2642  2eu2  2648  2eu5  2651  moeq3  3708  euabex  5461  nfunsn  6933  dff3  7101  fnoprabg  7533  zfrep6  7943  nqerf  10927  f1otrspeq  19317  uptx  23136  txcn  23137  pm14.12  43268  mndtcbas2  47793