MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eumo Structured version   Visualization version   GIF version

Theorem eumo 2647
Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.) Reduce axiom usage. (Revised by GL, 19-Feb-2022.)
Assertion
Ref Expression
eumo (∃!𝑥𝜑 → ∃*𝑥𝜑)

Proof of Theorem eumo
StepHypRef Expression
1 ax-1 6 . 2 (∃!𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑))
2 df-mo 2623 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
31, 2sylibr 224 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1852  ∃!weu 2618  ∃*wmo 2619
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 197  df-mo 2623
This theorem is referenced by:  eumoi  2649  euimmo  2671  moaneu  2682  eupick  2685  2eumo  2694  2exeu  2698  2eu2  2703  2eu5  2706  moeq3  3535  euabex  5057  nfunsn  6366  dff3  6515  fnoprabg  6908  zfrep6  7281  nqerf  9954  f1otrspeq  18074  uptx  21649  txcn  21650  pm14.12  39148
  Copyright terms: Public domain W3C validator