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 FFilX¬F

Proof

Step Hyp Ref Expression
1 filfbas FFilXFfBasX
2 0nelfb FfBasX¬F
3 1 2 syl FFilX¬F