Theorem eumo 2571

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

Syntax hints:   → wi 4  ∃wex 1779  ∃*wmo 2531  ∃!weu 2561

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 2562

This theorem is referenced by:  eumoi  2572  euimmo  2609  moaneu  2616  2exeuv  2625  eupick  2626  2eumo  2635  2exeu  2639  2eu2  2646  2eu5  2649  moeq3  3683  euabex  5421  nfunsn  6900  dff3  7072  fnoprabg  7512  zfrep6  7933  nqerf  10883  f1otrspeq  19377  uptx  23512  txcn  23513  pm14.12  44410  euendfunc  49515  arweuthinc  49518  arweutermc  49519  mndtcbas2  49572