Theorem eumo 2572

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

Syntax hints:   → wi 4  ∃wex 1779  ∃*wmo 2532  ∃!weu 2562

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 2563

This theorem is referenced by:  eumoi  2573  euimmo  2610  moaneu  2617  2exeuv  2626  eupick  2627  2eumo  2636  2exeu  2640  2eu2  2647  2eu5  2650  moeq3  3686  euabex  5424  nfunsn  6903  dff3  7075  fnoprabg  7515  zfrep6  7936  nqerf  10890  f1otrspeq  19384  uptx  23519  txcn  23520  pm14.12  44417  euendfunc  49519  arweuthinc  49522  arweutermc  49523  mndtcbas2  49576