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 496	1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1779  ∃*wmo 2538  ∃!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  3700  euabex  5441  nfunsn  6923  dff3  7095  fnoprabg  7535  zfrep6  7958  nqerf  10949  f1otrspeq  19433  uptx  23568  txcn  23569  pm14.12  44412  euendfunc  49378  arweuthinc  49381  arweutermc  49382  mndtcbas2  49427