Theorem eumo 2578

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

Syntax hints:   → wi 4  ∃wex 1779  ∃*wmo 2538  ∃!weu 2568

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 2569

This theorem is referenced by:  eumoi  2579  euimmo  2616  moaneu  2623  2exeuv  2632  eupick  2633  2eumo  2642  2exeu  2646  2eu2  2653  2eu5  2656  moeq3  3718  euabex  5466  nfunsn  6948  dff3  7120  fnoprabg  7556  zfrep6  7979  nqerf  10970  f1otrspeq  19465  uptx  23633  txcn  23634  pm14.12  44440  mndtcbas2  49180