Definition df-plusg 15165

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 15152	. 2 class +g
2		c2 10659	. . 3 class 2
3	2	cslot 15083	. 2 class Slot 2
4	1, 3	wceq 1437	1 wff +g = Slot 2

This definition is referenced by:  plusgndx  15186  plusgid  15187  grpstr  15195  grpbase  15196  grpplusg  15197  ressplusg  15198  frmdplusg  16589  oppradd  17793  sraaddg  18337  opsrplusg  18638  ply1plusgfvi  18770  zlmplusg  19021  znadd  19042  tngplusg  21581  ttgplusg  24754  resvplusg  28435  hlhilsplus  35219  mendplusgfval  35749