Metamath Proof Explorer


Syntax definition cvrgp

Description: Extend class notation with free group injection.

Ref Expression
Assertion cvrgp class var FGrp