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

Theorem eupick 2654
 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 2597 . 2 (∃!𝑥𝜑 → ∃*𝑥𝜑)
2 mopick 2646 . 2 ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))
31, 2sylan 583 1 ((∃!𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781  ∃*wmo 2555  ∃!weu 2587 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588 This theorem is referenced by:  eupicka  2655  eupickb  2656  reupick  4223  reupick3  4224  eusv2nf  5268  reusv2lem3  5273  copsexgw  5353  copsexg  5354  funssres  6384  oprabidw  7187  oprabid  7188  txcn  22339  isch3  29136  bnj849  32437  iotasbc  41531
 Copyright terms: Public domain W3C validator