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

Theorem eupick 2345
 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 2322 . 2
2 mopick 2344 . 2
31, 2sylan 459 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360  wex 1551  weu 2282  wmo 2283 This theorem is referenced by:  eupicka  2346  eupickb  2347  reupick  3626  reupick3  3627  copsexg  4443  eusv2nf  4722  reusv2lem3  4727  funssres  5494  oprabid  6106  txcn  17659  isch3  22745  iotasbc  27597  bnj849  29297 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287
 Copyright terms: Public domain W3C validator