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

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

Proof of Theorem eumo
StepHypRef Expression
1 df-eu 2651 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simprbi 497 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773  ∃*wmo 2617  ∃!weu 2650
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 2651
This theorem is referenced by:  eumoi  2661  euimmo  2698  moaneu  2706  2exeuv  2715  eupick  2716  2eumo  2725  2exeu  2729  2eu2  2736  2eu5  2740  2eu5OLD  2741  moeq3  3706  euabex  5349  nfunsn  6703  dff3  6861  fnoprabg  7268  zfrep6  7650  nqerf  10344  f1otrspeq  18498  uptx  22152  txcn  22153  pm14.12  40621
  Copyright terms: Public domain W3C validator