Theorem eupick 1411

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 1410	. 2 |- ((E*xph /\ E.x(ph /\ ps)) -> (ph -> ps))
2		eumo 1388	. 2 |- (E!xph -> E*xph)
3	1, 2	sylan 448	1 |- ((E!xph /\ E.x(ph /\ ps)) -> (ph -> ps))

Syntax hints:   -> wi 3   /\ wa 223  E.wex 956  E!weu 1357  E*wmo 1358

This theorem is referenced by:  eupickb 1412  reupick 2250  funssres 3492  tz6.12-1 3675  chcmh 9264

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360

Copyright terms: Public domain