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

Theorem eupick 2621
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 2564 . 2 (∃!𝑥𝜑 → ∃*𝑥𝜑)
2 mopick 2613 . 2 ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))
31, 2sylan 579 1 ((∃!𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1773  ∃*wmo 2524  ∃!weu 2554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-12 2163
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-nf 1778  df-mo 2526  df-eu 2555
This theorem is referenced by:  eupicka  2622  eupickb  2623  reupick  4310  reupick3  4311  eusv2nf  5383  reusv2lem3  5388  copsexgw  5480  copsexg  5481  funssres  6582  oprabidw  7432  oprabid  7433  txcn  23440  isch3  30918  bnj849  34391  iotasbc  43633
  Copyright terms: Public domain W3C validator