Theorem eumo 2612

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

Syntax hints:   → wi 4  ∃wex 1806  ∃*wmo 2571  ∃!weu 2602

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 210  df-an 401  df-eu 2603

This theorem is referenced by:  eumoi  2613  euimmo  2650  moaneu  2657  2exeuv  2666  eupick  2667  2eumo  2676  2exeu  2680  2eu2  2686  2eu5  2689  moeq3  3684  zfrep6  5251  euabex  5440  nfunsn  6918  dff3  7093  fnoprabg  7531  zfrep6OLD  7948  nqerf  10911  f1otrspeq  19513  uptx  23747  txcn  23748  bj-rep  37593  pm14.12  45016  euendfunc  50182  arweuthinc  50185  arweutermc  50186  mndtcbas2  50239