Metamath Proof Explorer


Syntax definition comu

Description: Extend the definition of a class to include the ordinal multiplication operation.

Ref Expression
Assertion comu class 𝑜