cplusg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cplusg		Structured version Visualization version GIF version

Syntax Definition cplusg 16888

Description: Extend class notation with group (addition) operation.

**Assertion**
Ref	Expression
cplusg	class +_g

See definition df-plusg 16901 for more information.

Colors of variables: wff setvar class