Theorem eupick

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 can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in WhiteheadRussell p. 192. (Contributed by NM, 10-Jul-1994)

	Ref	Expression
Assertion	eupick	$$⊢\left(\exists !x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\to \left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		eumo	$$⊢\exists !x\phi \to {\exists }^{*}x\phi$$
2		mopick	$$⊢\left({\exists }^{*}x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\to \left(\phi \to \psi \right)$$
3	1 2	sylan	$$⊢\left(\exists !x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\to \left(\phi \to \psi \right)$$