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

Theorem eumo 2338
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 2335 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
21simprbi 470 1  |-  ( E! x ph  ->  E* x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1673   E!weu 2309   E*wmo 2310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-eu 2313  df-mo 2314
This theorem is referenced by:  eumoi  2339  euimmo  2361  moaneu  2372  eupick  2375  2eumo  2384  2exeu  2388  2eu2  2393  2eu5  2396  moeq3  3226  euabex  4674  nfunsn  5918  dff3  6057  fnoprabg  6423  zfrep6  6787  nqerf  9380  f1otrspeq  17136  uptx  20688  txcn  20689  pm14.12  36815
  Copyright terms: Public domain W3C validator