Theorem eumo 2604

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  ∃*wmo 2563  ∃!weu 2594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2595

This theorem is used by:  eumoi  2605  euimmo  2642  moaneu  2649  2exeuv  2658  eupick  2659  2eumo  2668  2exeu  2672  2eu2  2678  2eu5  2681  moeq3  3670  zfrep6  5242  euabex  5429  nfunsn  6922  dff3  7098  fnoprabg  7541  zfrep6OLD  7965  nqerf  11008  f1otrspeq  19654  uptx  23937  txcn  23938  bj-rep  37969  pm14.12  45390  euendfunc  50603  arweuthinc  50606  arweutermc  50607  mndtcobeq  50660