df-plusg - Metamath Proof Explorer

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

Definition df-plusg 16001

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 15988	. 2 class +_g
2		c2 11108	. . 3 class 2
3	2	cslot 15903	. 2 class Slot 2
4	1, 3	wceq 1523	1 wff +_g = Slot 2

Colors of variables: wff setvar class

This definition is referenced by: plusgndx 16023 plusgid 16024 grpstr 16037 grpbase 16038 grpplusg 16039 ressplusg 16040 frmdplusg 17438 oppradd 18676 sraaddg 19227 opsrplusg 19528 ply1plusgfvi 19660 zlmplusg 19915 znadd 19937 tngplusg 22493 ttgplusg 25803 resvplusg 29961 hlhilsplus 37549 mendplusgfval 38072