|Metamath Proof Explorer
|Mirrors > Home > MPE Home > Th. List > cresc
|Structured version Visualization version GIF version
|Description: Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms).
|Colors of variables: wff setvar class
|Copyright terms: Public domain