Theorem eumo 2608

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

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

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 2599

This theorem is used by:  eumoi  2609  euimmo  2646  moaneu  2653  2exeuv  2662  eupick  2663  2eumo  2672  2exeu  2676  2eu2  2682  2eu5  2685  moeq3  3677  zfrep6  5252  euabex  5444  nfunsn  6924  dff3  7099  fnoprabg  7539  zfrep6OLD  7954  nqerf  10926  f1otrspeq  19540  uptx  23811  txcn  23812  bj-rep  37743  pm14.12  45164  euendfunc  50337  arweuthinc  50340  arweutermc  50341  mndtcbas2  50394