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

Theorem eupick 2206
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 2183 . 2  |-  ( E! x ph  ->  E* x ph )
2 mopick 2205 . 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 1528   E!weu 2143   E*wmo 2144
This theorem is referenced by:  eupicka  2207  eupickb  2208  reupick  3452  reupick3  3453  copsexg  4252  eusv2nf  4532  reusv2lem3  4537  funssres  5294  oprabid  5882  txcn  17320  isch3  21821  copsexgb  24966  iotasbc  27619  bnj849  28957
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148
  Copyright terms: Public domain W3C validator