This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupicka

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

		Ref	Expression
	Assertion	eupicka	$⊢ (\exists! x φ \land \exists x (φ \land ψ)) \to \forall x (φ \to ψ)$

Step	Hyp	Ref	Expression
1		nfeu1	$⊢ Ⅎ x \exists! x φ$
2		nfe1	$⊢ Ⅎ x \exists x (φ \land ψ)$
3	1 2	nfan	$⊢ Ⅎ x (\exists! x φ \land \exists x (φ \land ψ))$
4		eupick	$⊢ (\exists! x φ \land \exists x (φ \land ψ)) \to (φ \to ψ)$
5	3 4	alrimi	$⊢ (\exists! x φ \land \exists x (φ \land ψ)) \to \forall x (φ \to ψ)$