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  4850  nfunsn  6120  dff3  6265  fnoprabg  6637  zfrep6  7005  nqerf  9609  f1otrspeq  17639  uptx  21186  txcn  21187  pm14.12  37438
  Copyright terms: Public domain W3C validator