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

Theorem eupick 2358
 Description: Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing such that is true, and there is also an (actually the same one) such that and are both true, then implies regardless of . 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

Proof of Theorem eupick
StepHypRef Expression
1 eumo 2313 . 2
2 mopick 2356 . 2
31, 2sylan 471 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  E!weu 2282  E*wmo 2283 This theorem is referenced by:  eupicka  2359  eupickb  2360  reupick  3781  reupick3  3782  eusv2nf  4650  reusv2lem3  4655  copsexg  4737  copsexgOLD  4738  funssres  5633  oprabid  6323  txcn  20127  isch3  26159  iotasbc  31326  bnj849  33983 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287
 Copyright terms: Public domain W3C validator