Theorem eumo 2606

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

Syntax hints:   → wi 4  ∃wex 1809  ∃*wmo 2565  ∃!weu 2596

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 210  df-an 401  df-eu 2597

This theorem is referenced by:  eumoi  2607  euimmo  2644  moaneu  2651  2exeuv  2660  eupick  2661  2eumo  2670  2exeu  2674  2eu2  2680  2eu5  2683  moeq3  3676  zfrep6  5251  euabex  5444  nfunsn  6922  dff3  7097  fnoprabg  7535  zfrep6OLD  7953  nqerf  10916  f1otrspeq  19518  uptx  23763  txcn  23764  bj-rep  37691  pm14.12  45114  euendfunc  50287  arweuthinc  50290  arweutermc  50291  mndtcbas2  50344