Theorem eumo 2581

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

Syntax hints:   → wi 4  ∃wex 1777  ∃*wmo 2541  ∃!weu 2571

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 207  df-an 396  df-eu 2572

This theorem is referenced by:  eumoi  2582  euimmo  2619  moaneu  2626  2exeuv  2635  eupick  2636  2eumo  2645  2exeu  2649  2eu2  2656  2eu5  2659  moeq3  3734  euabex  5481  nfunsn  6962  dff3  7134  fnoprabg  7573  zfrep6  7995  nqerf  10999  f1otrspeq  19489  uptx  23654  txcn  23655  pm14.12  44390  mndtcbas2  48756