Metamath Proof Explorer

Syntax definition cur

Description: Extend class notation with ring unit.

Ref Expression
Assertion cur 
class 1r