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

Metamath Proof Explorer

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	$⊢ (F \in Fil (X) \land A \in F) \to A \neq \emptyset$

Step	Hyp	Ref	Expression
1		id	$⊢ A \in F \to A \in F$
2		0nelfil	$⊢ F \in Fil (X) \to \neg \emptyset \in F$
3		nelne2	$⊢ (A \in F \land \neg \emptyset \in F) \to A \neq \emptyset$
4	1 2 3	syl2anr	$⊢ (F \in Fil (X) \land A \in F) \to A \neq \emptyset$