Theorem eumo 2576

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

Syntax hints:   → wi 4  ∃wex 1776  ∃*wmo 2536  ∃!weu 2566

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 2567

This theorem is referenced by:  eumoi  2577  euimmo  2614  moaneu  2621  2exeuv  2630  eupick  2631  2eumo  2640  2exeu  2644  2eu2  2651  2eu5  2654  moeq3  3721  euabex  5472  nfunsn  6949  dff3  7120  fnoprabg  7556  zfrep6  7978  nqerf  10968  f1otrspeq  19480  uptx  23649  txcn  23650  pm14.12  44417  mndtcbas2  48892