Metamath Proof Explorer


Syntax definition cefg

Description: Extend class notation with the free group equivalence relation.

Ref Expression
Assertion cefg class ~FG