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

Theorem eupick 2345
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 2322 . 2  |-  ( E! x ph  ->  E* x ph )
2 mopick 2344 . 2  |-  ( ( E* x ph  /\  E. x ( ph  /\  ps ) )  ->  ( ph  ->  ps ) )
31, 2sylan 459 1  |-  ( ( E! x ph  /\  E. x ( ph  /\  ps ) )  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551   E!weu 2282   E*wmo 2283
This theorem is referenced by:  eupicka  2346  eupickb  2347  reupick  3626  reupick3  3627  copsexg  4443  eusv2nf  4722  reusv2lem3  4727  funssres  5494  oprabid  6106  txcn  17659  isch3  22745  iotasbc  27597  bnj849  29297
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator