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  3680  euabex  5416  nfunsn  6882  dff3  7054  fnoprabg  7492  zfrep6  7913  nqerf  10859  f1otrspeq  19353  uptx  23488  txcn  23489  pm14.12  44383  euendfunc  49488  arweuthinc  49491  arweutermc  49492  mndtcbas2  49545