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

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

Proof of Theorem eumo
StepHypRef Expression
1 df-eu 2569 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simprbi 496 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1779  ∃*wmo 2538  ∃!weu 2568
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 207  df-an 396  df-eu 2569
This theorem is referenced by:  eumoi  2579  euimmo  2616  moaneu  2623  2exeuv  2632  eupick  2633  2eumo  2642  2exeu  2646  2eu2  2653  2eu5  2656  moeq3  3718  euabex  5466  nfunsn  6948  dff3  7120  fnoprabg  7556  zfrep6  7979  nqerf  10970  f1otrspeq  19465  uptx  23633  txcn  23634  pm14.12  44440  mndtcbas2  49180
  Copyright terms: Public domain W3C validator