Theorem eupick 1055

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

Syntax hints:   -> wi 2   /\ wa 196  E.wex 678  E!weu 1007  E*wmo 1008

This theorem is referenced by:  eupickb 1056  reupick 1578  funssres 2698  tz6.12-1 2842  chcmh 5148

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010

metamath.org