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 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 2183 . 2
2 mopick 2205 . 2
31, 2sylan 457 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358  wex 1528  weu 2143  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