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 e. ( Fil ` X ) /\ A e. F ) -> A C_ X )

Proof

Step Hyp Ref Expression
1 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2 fbelss 
 |-  ( ( F e. ( fBas ` X ) /\ A e. F ) -> A C_ X )
3 1 2 sylan 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> A C_ X )