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

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

Proof of Theorem eumo
StepHypRef Expression
1 df-eu 2567 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simprbi 497 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1780  ∃*wmo 2536  ∃!weu 2566
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 206  df-an 397  df-eu 2567
This theorem is referenced by:  eumoi  2577  euimmo  2616  moaneu  2623  2exeuv  2632  eupick  2633  2eumo  2642  2exeu  2646  2eu2  2652  2eu5  2655  moeq3  3658  euabex  5406  nfunsn  6867  dff3  7032  fnoprabg  7459  zfrep6  7865  nqerf  10787  f1otrspeq  19151  uptx  22882  txcn  22883  pm14.12  42360  mndtcbas2  46721
  Copyright terms: Public domain W3C validator