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

Theorem eupick 2179
 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 2156 . 2
2 mopick 2178 . 2
31, 2sylan 459 1
 Colors of variables: wff set class Syntax hints:   wi 6   wa 360  wex 1537  weu 2117  wmo 2118 This theorem is referenced by:  eupicka  2180  eupickb  2181  reupick  3394  reupick3  3395  copsexg  4189  eusv2nf  4469  reusv2lem3  4474  funssres  5197  tz6.12-1  5442  oprabid  5781  txcn  17247  isch3  21746  copsexgb  24297  iotasbc  26952  bnj849  27969 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122
 Copyright terms: Public domain W3C validator