Theorem eupicka

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

	Ref	Expression
Assertion	eupicka	⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfeu1	⊢ Ⅎ 𝑥 ∃! 𝑥 𝜑
2		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝜑 ∧ 𝜓 )
3	1 2	nfan	⊢ Ⅎ 𝑥 ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
4		eupick	⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 → 𝜓 ) )
5	3 4	alrimi	⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) )