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	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		filfbas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2		fbelss	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ 𝑋 )
3	1 2	sylan	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → 𝐴 ⊆ 𝑋 )