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 1780  ∃*wmo 2537  ∃!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  3670  euabex  5409  nfunsn  6873  dff3  7045  fnoprabg  7481  zfrep6  7899  nqerf  10841  f1otrspeq  19376  uptx  23569  txcn  23570  pm14.12  44662  euendfunc  49771  arweuthinc  49774  arweutermc  49775  mndtcbas2  49828