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

Theorem eumo 2320
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 2318 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
21simprbi 451 1  |-  ( E! x ph  ->  E* x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550   E!weu 2280   E*wmo 2281
This theorem is referenced by:  eumoi  2321  euimmo  2329  moaneu  2339  eupick  2343  2eumo  2353  2exeu  2357  2eu2  2361  2eu5  2364  moeq3  3103  euabex  4416  nfunsn  5753  dff3  5874  zfrep6  5960  fnoprabg  6163  nqerf  8799  uptx  17649  txcn  17650  f1otrspeq  27358  pm14.12  27589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285
  Copyright terms: Public domain W3C validator