Theorem eupick 2664

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

Step	Hyp	Ref	Expression
1		eumo 2609	. 2 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)
2		mopick 2656	. 2 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))
3	1, 2	sylan 592	1 ⊢ ((∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812  ∃*wmo 2568  ∃!weu 2599

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2570  df-eu 2600

This theorem is used by:  eupicka  2665  eupickb  2666  reupick  4285  reupick3  4286  eusv2nf  5371  reusv2lem3  5376  copsexgw  5477  copsexgwOLD  5478  copsexg  5479  funssres  6587  oprabidw  7454  oprabid  7455  txcn  23820  isch3  31630  bnj849  35345  iotasbc  45170