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

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

Proof of Theorem eumo
StepHypRef Expression
1 df-eu 2647 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simprbi 497 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1771  ∃*wmo 2613  ∃!weu 2646
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 208  df-an 397  df-eu 2647
This theorem is referenced by:  eumoi  2657  euimmo  2693  moaneu  2701  2exeuv  2710  eupick  2711  2eumo  2720  2exeu  2724  2eu2  2731  2eu5  2735  2eu5OLD  2736  moeq3  3700  euabex  5344  nfunsn  6700  dff3  6858  fnoprabg  7264  zfrep6  7645  nqerf  10340  f1otrspeq  18504  uptx  22161  txcn  22162  pm14.12  40630
  Copyright terms: Public domain W3C validator