Theorem eumo 2579

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

Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2538  ∃!weu 2569

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 2570

This theorem is referenced by:  eumoi  2580  euimmo  2617  moaneu  2624  2exeuv  2633  eupick  2634  2eumo  2643  2exeu  2647  2eu2  2654  2eu5  2657  moeq3  3672  euabex  5416  nfunsn  6881  dff3  7054  fnoprabg  7491  zfrep6  7909  nqerf  10853  f1otrspeq  19388  uptx  23581  txcn  23582  bj-rep  37318  pm14.12  44774  euendfunc  49882  arweuthinc  49885  arweutermc  49886  mndtcbas2  49939