Theorem eumo 2575

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

Syntax hints:   → wi 4  ∃wex 1780  ∃*wmo 2535  ∃!weu 2565

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 2566

This theorem is referenced by:  eumoi  2576  euimmo  2613  moaneu  2620  2exeuv  2629  eupick  2630  2eumo  2639  2exeu  2643  2eu2  2650  2eu5  2653  moeq3  3667  euabex  5406  nfunsn  6870  dff3  7042  fnoprabg  7478  zfrep6  7896  nqerf  10832  f1otrspeq  19367  uptx  23560  txcn  23561  pm14.12  44578  euendfunc  49687  arweuthinc  49690  arweutermc  49691  mndtcbas2  49744