Definition df-plusg 13497

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 13484	. 2 class +g
2		c2 10005	. . 3 class 2
3	2	cslot 13423	. 2 class Slot 2
4	1, 3	wceq 1649	1 wff +g = Slot 2

This definition is referenced by:  plusgndx  13518  plusgid  13519  grpstr  13523  grpbase  13524  grpplusg  13525  ressplusg  13526  frmdplusg  14754  oppradd  15690  sraaddg  16206  opsrplusg  16495  ply1plusgfvi  16591  zlmplusg  16755  znadd  16776  tngplusg  18636  mendplusgfval  27361  hlhilsplus  32426