Metamath Proof Explorer


Theorem filfbas

Description: A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion filfbas FFilXFfBasX

Proof

Step Hyp Ref Expression
1 isfil FFilXFfBasXx𝒫XF𝒫xxF
2 1 simplbi FFilXFfBasX