Theorem eumo 2499

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

Syntax hints:   → wi 4  ∃wex 1704  ∃!weu 2470  ∃*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-eu 2474  df-mo 2475

This theorem is referenced by:  eumoi  2500  euimmo  2522  moaneu  2533  eupick  2536  2eumo  2545  2exeu  2549  2eu2  2554  2eu5  2557  moeq3  3383  euabex  4929  nfunsn  6225  dff3  6372  fnoprabg  6761  zfrep6  7134  nqerf  9752  f1otrspeq  17867  uptx  21428  txcn  21429  pm14.12  38622