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	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\right)\to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in F\to A\in F$$
2		0nelfil	$$⊢F\in \mathrm{Fil}\left(X\right)\to \neg \varnothing \in F$$
3		nelne2	$$⊢\left(A\in F\wedge \neg \varnothing \in F\right)\to A\ne \varnothing$$
4	1 2 3	syl2anr	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge A\in F\right)\to A\ne \varnothing$$