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  7530  zfrep6  7940  nqerf  10924  f1otrspeq  19314  uptx  23128  txcn  23129  pm14.12  43170  mndtcbas2  47699