Metamath Proof Explorer


Syntax definition cnumer

Description: Extend class notation to include canonical numerator function.

Ref Expression
Assertion cnumer class numer