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

Theorem eupick 2219
Description: Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing  x such that 
ph is true, and there is also an  x (actually the same one) such that  ph and  ps are both true, then  ph implies  ps regardless of  x. This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by NM, 10-Jul-1994.)
Assertion
Ref Expression
eupick  |-  ( ( E! x ph  /\  E. x ( ph  /\  ps ) )  ->  ( ph  ->  ps ) )

Proof of Theorem eupick
StepHypRef Expression
1 eumo 2196 . 2  |-  ( E! x ph  ->  E* x ph )
2 mopick 2218 . 2  |-  ( ( E* x ph  /\  E. x ( ph  /\  ps ) )  ->  ( ph  ->  ps ) )
31, 2sylan 457 1  |-  ( ( E! x ph  /\  E. x ( ph  /\  ps ) )  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531   E!weu 2156   E*wmo 2157
This theorem is referenced by:  eupicka  2220  eupickb  2221  reupick  3465  reupick3  3466  copsexg  4268  eusv2nf  4548  reusv2lem3  4553  funssres  5310  oprabid  5898  txcn  17336  isch3  21837  copsexgb  25069  iotasbc  27722  bnj849  29273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161
  Copyright terms: Public domain W3C validator