Metamath Proof Explorer

Theorem 0nelfil

Description: The empty set doesn't belong to a filter. (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion 0nelfil 
|- ( F e. ( Fil ` X ) -> -. (/) e. F )

Proof

Step Hyp Ref Expression
1 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2 0nelfb 
 |-  ( F e. ( fBas ` X ) -> -. (/) e. F )
3 1 2 syl 
 |-  ( F e. ( Fil ` X ) -> -. (/) e. F )