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  3659  zfrep6  5224  euabex  5408  nfunsn  6873  dff3  7046  fnoprabg  7483  zfrep6OLD  7901  nqerf  10844  f1otrspeq  19413  uptx  23600  txcn  23601  bj-rep  37396  pm14.12  44866  euendfunc  50013  arweuthinc  50016  arweutermc  50017  mndtcbas2  50070