NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eupick Unicode version

Theorem eupick 2267
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 2244 . 2
2 mopick 2266 . 2
31, 2sylan 457 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358  wex 1541  weu 2204  wmo 2205
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209
This theorem is referenced by:  eupicka  2268  eupickb  2269  reupick  3539  reupick3  3540  copsexg  4607  funssres  5144  oprabid  5550
  Copyright terms: Public domain W3C validator