Metamath Proof Explorer


Syntax definition cthinc

Description: Extend class notation with the class of thin categories.

Ref Expression
Assertion cthinc class ThinCat