Theorem eumo 2573

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

Syntax hints:   → wi 4  ∃wex 1780  ∃*wmo 2533  ∃!weu 2563

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 2564

This theorem is referenced by:  eumoi  2574  euimmo  2611  moaneu  2618  2exeuv  2627  eupick  2628  2eumo  2637  2exeu  2641  2eu2  2648  2eu5  2651  moeq3  3671  euabex  5401  nfunsn  6861  dff3  7033  fnoprabg  7469  zfrep6  7887  nqerf  10821  f1otrspeq  19360  uptx  23541  txcn  23542  pm14.12  44460  euendfunc  49564  arweuthinc  49567  arweutermc  49568  mndtcbas2  49621