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 1811  ∃*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  3669  zfrep6  5241  euabex  5428  nfunsn  6925  dff3  7101  fnoprabg  7544  zfrep6OLD  7968  nqerf  11019  f1otrspeq  19667  uptx  23950  txcn  23951  bj-rep  38082  pm14.12  45499  euendfunc  50755  arweuthinc  50758  arweutermc  50759  mndtcobeq  50815