Theorem eumo 2647

Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.) Reduce axiom usage. (Revised by GL, 19-Feb-2022.)

Assertion

Ref	Expression
eumo	⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

Proof of Theorem eumo

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (∃!𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑))
2		df-mo 2623	. 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
3	1, 2	sylibr 224	1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1852  ∃!weu 2618  ∃*wmo 2619

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 197  df-mo 2623

This theorem is referenced by:  eumoi  2649  euimmo  2671  moaneu  2682  eupick  2685  2eumo  2694  2exeu  2698  2eu2  2703  2eu5  2706  moeq3  3535  euabex  5057  nfunsn  6366  dff3  6515  fnoprabg  6908  zfrep6  7281  nqerf  9954  f1otrspeq  18074  uptx  21649  txcn  21650  pm14.12  39148