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

Theorem eumo 2183
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 2181 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
21simprbi 450 1  |-  ( E! x ph  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528   E!weu 2143   E*wmo 2144
This theorem is referenced by:  eumoi  2184  euimmo  2192  moaneu  2202  eupick  2206  2eumo  2216  2exeu  2220  2eu2  2224  2eu5  2227  moeq3  2942  euabex  4234  nfunsn  5558  dff3  5673  zfrep6  5748  fnoprabg  5945  nqerf  8554  uptx  17319  txcn  17320  f1otrspeq  27390  pm14.12  27621
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator