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

Theorem eumo 2636
 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 2612 . 2 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
31, 2sylibr 224 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1853  ∃!weu 2607  ∃*wmo 2608 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 2612 This theorem is referenced by:  eumoi  2638  euimmo  2660  moaneu  2671  eupick  2674  2eumo  2683  2exeu  2687  2eu2  2692  2eu5  2695  moeq3  3524  euabex  5078  nfunsn  6386  dff3  6535  fnoprabg  6926  zfrep6  7299  nqerf  9944  f1otrspeq  18067  uptx  21630  txcn  21631  pm14.12  39124
 Copyright terms: Public domain W3C validator