Theorem eupicka

Description: Version of eupick with closed formulas. (Contributed by NM, 6-Sep-2008)

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

Proof

Step	Hyp	Ref	Expression
1		nfeu1	$$⊢Ⅎx\exists !x\phi$$
2		nfe1	$$⊢Ⅎx\exists x\left(\phi \wedge \psi \right)$$
3	1 2	nfan	$$⊢Ⅎx\left(\exists !x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)$$
4		eupick	$$⊢\left(\exists !x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\to \left(\phi \to \psi \right)$$
5	3 4	alrimi	$$⊢\left(\exists !x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\to \forall x\left(\phi \to \psi \right)$$