Metamath Proof Explorer


Syntax definition cmndo

Description: Extend class notation with the class of all monoids.

Ref Expression
Assertion cmndo class MndOp