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

Theorem eupick 2336
 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 2297 . 2
2 mopick 2334 . 2
31, 2sylan 473 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370  wex 1659  weu 2266  wmo 2267 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907  ax-13 2055 This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-eu 2270  df-mo 2271 This theorem is referenced by:  eupicka  2337  eupickb  2338  reupick  3763  reupick3  3764  eusv2nf  4623  reusv2lem3  4628  copsexg  4707  funssres  5641  oprabid  6332  txcn  20572  isch3  26729  bnj849  29524  iotasbc  36407
 Copyright terms: Public domain W3C validator