Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eupick Unicode version

Theorem eupick 2079
 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 2032 . 2
2 mopick 2078 . 2
31, 2sylan 281 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103  wex 1469  weu 2000  wmo 2001 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004 This theorem is referenced by:  eupicka  2080  eupickb  2081  reupick  3366  reupick3  3367  copsexg  4175  eusv2nf  4386  funssres  5174  oprabid  5812  txcn  12503
 Copyright terms: Public domain W3C validator