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

Theorem eumo 2487
Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
eumo (∃!𝑥𝜑 → ∃*𝑥𝜑)

Proof of Theorem eumo
StepHypRef Expression
1 eu5 2484 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simprbi 479 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1695  ∃!weu 2458  ∃*wmo 2459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-eu 2462  df-mo 2463
This theorem is referenced by:  eumoi  2488  euimmo  2510  moaneu  2521  eupick  2524  2eumo  2533  2exeu  2537  2eu2  2542  2eu5  2545  moeq3  3350  euabex  4856  nfunsn  6135  dff3  6280  fnoprabg  6659  zfrep6  7027  nqerf  9631  f1otrspeq  17690  uptx  21238  txcn  21239  pm14.12  37644
  Copyright terms: Public domain W3C validator