Metamath Proof Explorer

Syntax definition crngc

Description: Extend class notation to include the category Rng.

Ref Expression
Assertion crngc class RngCat