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

Theorem eupick 2629
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 2572 . 2 (∃!𝑥𝜑 → ∃*𝑥𝜑)
2 mopick 2621 . 2 ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))
31, 2sylan 580 1 ((∃!𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1781  ∃*wmo 2532  ∃!weu 2562
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 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-mo 2534  df-eu 2563
This theorem is referenced by:  eupicka  2630  eupickb  2631  reupick  4318  reupick3  4319  eusv2nf  5393  reusv2lem3  5398  copsexgw  5490  copsexg  5491  funssres  6592  oprabidw  7442  oprabid  7443  txcn  23350  isch3  30749  bnj849  34222  iotasbc  43480
  Copyright terms: Public domain W3C validator