Theorem eumo 2579

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

Syntax hints:   → wi 4  ∃wex 1785  ∃*wmo 2539  ∃!weu 2569

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 2570

This theorem is referenced by:  eumoi  2580  euimmo  2619  moaneu  2626  2exeuv  2635  eupick  2636  2eumo  2645  2exeu  2649  2eu2  2655  2eu5  2658  moeq3  3650  euabex  5378  nfunsn  6805  dff3  6970  fnoprabg  7388  zfrep6  7784  nqerf  10670  f1otrspeq  19036  uptx  22757  txcn  22758  pm14.12  41992  mndtcbas2  46322