Metamath Proof Explorer


Syntax definition cresc

Description: Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms).

Ref Expression
Assertion cresc
class |`cat