Theorem eumo 2604

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

Syntax hints:   → wi 4  ∃wex 1798  ∃*wmo 2563  ∃!weu 2594

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 209  df-an 400  df-eu 2595

This theorem is referenced by:  eumoi  2605  euimmo  2642  moaneu  2649  2exeuv  2658  eupick  2659  2eumo  2668  2exeu  2672  2eu2  2678  2eu5  2681  moeq3  3673  zfrep6  5236  euabex  5425  nfunsn  6901  dff3  7076  fnoprabg  7514  zfrep6OLD  7931  nqerf  10882  f1otrspeq  19478  uptx  23673  txcn  23674  bj-rep  37519  pm14.12  44958  euendfunc  50108  arweuthinc  50111  arweutermc  50112  mndtcbas2  50165