Metamath Proof Explorer


Syntax definition cgrp

Description: Extend class notation with class of all groups.

Ref Expression
Assertion cgrp class Grp