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  5406  nfunsn  6871  dff3  7044  fnoprabg  7481  zfrep6OLD  7899  nqerf  10842  f1otrspeq  19411  uptx  23599  txcn  23600  bj-rep  37393  pm14.12  44863  euendfunc  49998  arweuthinc  50001  arweutermc  50002  mndtcbas2  50055