Theorem 0nelfil

Description: The empty set doesn't belong to a filter. (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)

	Ref	Expression
Assertion	0nelfil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		filfbas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2		0nelfb	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
3	1 2	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )