Definition df-plusg 15202

Description: Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)

Assertion

Ref	Expression
df-plusg	|- +g = Slot 2

Detailed syntax breakdown of Definition df-plusg

Step	Hyp	Ref	Expression
1		cplusg 15189	. 2 class +g
2		c2 10666	. . 3 class 2
3	2	cslot 15119	. 2 class Slot 2
4	1, 3	wceq 1437	1 wff +g = Slot 2

This definition is referenced by:  plusgndx  15223  plusgid  15224  grpstr  15235  grpbase  15236  grpplusg  15237  ressplusg  15238  frmdplusg  16637  oppradd  17857  sraaddg  18401  opsrplusg  18702  ply1plusgfvi  18834  zlmplusg  19088  znadd  19109  tngplusg  21648  ttgplusg  24906  resvplusg  28604  hlhilsplus  35480  mendplusgfval  36021