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

Theorem eumo 2184
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 2182 . 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 1529   E!weu 2144   E*wmo 2145
This theorem is referenced by:  eumoi  2185  euimmo  2193  moaneu  2203  eupick  2207  2eumo  2217  2exeu  2221  2eu2  2225  2eu5  2228  moeq3  2943  euabex  4233  nfunsn  5519  dff3  5634  zfrep6  5709  fnoprabg  5906  nqerf  8549  uptx  17313  txcn  17314  f1otrspeq  26789  pm14.12  27020
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149
  Copyright terms: Public domain W3C validator