Theorem eumo 2571

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

Syntax hints:   → wi 4  ∃wex 1780  ∃*wmo 2531  ∃!weu 2561

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 396  df-eu 2562

This theorem is referenced by:  eumoi  2572  euimmo  2611  moaneu  2618  2exeuv  2627  eupick  2628  2eumo  2637  2exeu  2641  2eu2  2647  2eu5  2650  moeq3  3708  euabex  5461  nfunsn  6933  dff3  7101  fnoprabg  7534  zfrep6  7945  nqerf  10931  f1otrspeq  19363  uptx  23448  txcn  23449  pm14.12  43642  mndtcbas2  47870