Theorem eumo 2603

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  ∃*wmo 2562  ∃!weu 2593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2594

This theorem is used by:  eumoi  2604  euimmo  2641  moaneu  2648  2exeuv  2657  eupick  2658  2eumo  2667  2exeu  2671  2eu2  2677  2eu5  2680  moeq3  3670  zfrep6  5244  euabex  5436  nfunsn  6917  dff3  7093  fnoprabg  7536  zfrep6OLD  7952  nqerf  10939  f1otrspeq  19574  uptx  23851  txcn  23852  bj-rep  37818  pm14.12  45245  euendfunc  50452  arweuthinc  50455  arweutermc  50456  mndtcbas2  50509