Theorem eumo 2578

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

Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2537  ∃!weu 2568

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 2569

This theorem is referenced by:  eumoi  2579  euimmo  2616  moaneu  2623  2exeuv  2632  eupick  2633  2eumo  2642  2exeu  2646  2eu2  2653  2eu5  2656  moeq3  3658  zfrep6  5224  euabex  5413  nfunsn  6879  dff3  7052  fnoprabg  7490  zfrep6OLD  7908  nqerf  10853  f1otrspeq  19422  uptx  23590  txcn  23591  bj-rep  37380  pm14.12  44848  euendfunc  50001  arweuthinc  50004  arweutermc  50005  mndtcbas2  50058