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

Theorem eumo 2156
Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
eumo  |-  ( E! x ph  ->  E* x ph )

Proof of Theorem eumo
StepHypRef Expression
1 eu5 2154 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
21simprbi 452 1  |-  ( E! x ph  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537   E!weu 2117   E*wmo 2118
This theorem is referenced by:  eumoi  2157  euimmo  2165  moaneu  2175  eupick  2179  2eumo  2189  2exeu  2193  2eu2  2197  2eu5  2200  moeq3  2910  euabex  4192  nfunsn  5478  dff3  5593  zfrep6  5668  fnoprabg  5865  nqerf  8508  uptx  17267  txcn  17268  f1otrspeq  26743  pm14.12  26975
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122
  Copyright terms: Public domain W3C validator