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  3674  euabex  5408  nfunsn  6866  dff3  7038  fnoprabg  7476  zfrep6  7897  nqerf  10843  f1otrspeq  19344  uptx  23528  txcn  23529  pm14.12  44397  euendfunc  49515  arweuthinc  49518  arweutermc  49519  mndtcbas2  49572