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

Theorem eumo 2315
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 2312 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
21simprbi 462 1  |-  ( E! x ph  ->  E* x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1617   E!weu 2284   E*wmo 2285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-eu 2288  df-mo 2289
This theorem is referenced by:  eumoi  2316  euimmo  2340  moaneu  2351  eupick  2355  2eumo  2364  2exeu  2368  2eu2  2375  2eu5  2379  moeq3  3273  euabex  4698  nfunsn  5879  dff3  6020  fnoprabg  6376  zfrep6  6741  nqerf  9297  f1otrspeq  16674  uptx  20295  txcn  20296  pm14.12  31572
  Copyright terms: Public domain W3C validator