Metamath Proof Explorer

Syntax definition cinvr

Description: Extend class notation with multiplicative inverse.

Ref Expression
Assertion cinvr 
class invr