Metamath Proof Explorer


Syntax definition clmod

Description: Extend class notation with class of all left modules.

Ref Expression
Assertion clmod class LMod