Theorem eupick 1436

Description: Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing x such that ph is true, and there is also an x (actually the same one) such that ph and ps are both true, then ph implies ps regardless of x. This theorem, which apparently does not appear explicitly in the literature, can be quite useful because it lets us eliminate existential quantifiers in a hypothesis.

Assertion

Ref	Expression
eupick	|- ((E!xph /\ E.x(ph /\ ps)) -> (ph -> ps))

Proof of Theorem eupick

Step	Hyp	Ref	Expression
1		mopick 1435	. 2 |- ((E*xph /\ E.x(ph /\ ps)) -> (ph -> ps))
2		eumo 1413	. 2 |- (E!xph -> E*xph)
3	1, 2	sylan 450	1 |- ((E!xph /\ E.x(ph /\ ps)) -> (ph -> ps))

Syntax hints:   -> wi 3   /\ wa 223  E.wex 982  E!weu 1382  E*wmo 1383

This theorem is referenced by:  eupicka 1437  eupickb 1438  reupick 2283  funssres 3559  tz6.12-1 3743  chcmh 9115

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385

Copyright terms: Public domain