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

Theorem eumo 2153
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 2151 . 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 2114   E*wmo 2115
This theorem is referenced by:  eumoi  2154  euimmo  2162  moaneu  2172  eupick  2176  2eumo  2186  2exeu  2190  2eu2  2194  2eu5  2197  moeq3  2879  euabex  4127  reuxfrd  4450  nfunsn  5410  dff3  5525  zfrep6  5600  fnoprabg  5797  nqerf  8434  uptx  17151  txcn  17152  f1otrspeq  26556  pm14.12  26788
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 1926
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 1883  df-eu 2118  df-mo 2119
  Copyright terms: Public domain W3C validator