Theorem eupick 2663

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 2608	. 2 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)
2		mopick 2655	. 2 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))
3	1, 2	sylan 591	1 ⊢ ((∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1802  ∃*wmo 2567  ∃!weu 2598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-mo 2569  df-eu 2599

This theorem is referenced by:  eupicka  2664  eupickb  2665  reupick  4284  reupick3  4285  eusv2nf  5356  reusv2lem3  5361  copsexgw  5462  copsexgwOLD  5463  copsexg  5464  funssres  6569  oprabidw  7431  oprabid  7432  txcn  23740  isch3  31498  bnj849  35225  iotasbc  44988