Theorem eumo 2497

Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)

Assertion

Ref	Expression
eumo	⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

Proof of Theorem eumo

Step	Hyp	Ref	Expression
1		eu5 2494	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2	1	simprbi 480	1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1702  ∃!weu 2468  ∃*wmo 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-eu 2472  df-mo 2473

This theorem is referenced by:  eumoi  2498  euimmo  2520  moaneu  2531  eupick  2534  2eumo  2543  2exeu  2547  2eu2  2552  2eu5  2555  moeq3  3377  euabex  4920  nfunsn  6212  dff3  6358  fnoprabg  6746  zfrep6  7119  nqerf  9737  f1otrspeq  17848  uptx  21409  txcn  21410  pm14.12  38442