Metamath Proof Explorer


Syntax definition cfil

Description: Extend class notation with the set of filters on a set.

Ref Expression
Assertion cfil
class Fil