Theorem fileln0

Description: An element of a filter is nonempty. (Contributed by FL, 24-May-2011) (Revised by Mario Carneiro, 28-Jul-2015)

	Ref	Expression
Assertion	fileln0	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ 𝐹 → 𝐴 ∈ 𝐹 )
2		0nelfil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
3		nelne2	⊢ ( ( 𝐴 ∈ 𝐹 ∧ ¬ ∅ ∈ 𝐹 ) → 𝐴 ≠ ∅ )
4	1 2 3	syl2anr	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ≠ ∅ )