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

Metamath Proof Explorer

Theorem filelss

Description: An element of a filter is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	filelss	$⊢ (F \in Fil (X) \land A \in F) \to A \subseteq X$

Step	Hyp	Ref	Expression
1		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
2		fbelss	$⊢ (F \in fBas (X) \land A \in F) \to A \subseteq X$
3	1 2	sylan	$⊢ (F \in Fil (X) \land A \in F) \to A \subseteq X$