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 15781

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 15768	. 2 class +_g
2		c2 10947	. . 3 class 2
3	2	cslot 15694	. 2 class Slot 2
4	1, 3	wceq 1475	1 wff +_g = Slot 2

Colors of variables: wff setvar class

This definition is referenced by: plusgndx 15803 plusgid 15804 grpstr 15815 grpbase 15816 grpplusg 15817 ressplusg 15818 frmdplusg 17214 oppradd 18453 sraaddg 19000 opsrplusg 19301 ply1plusgfvi 19433 zlmplusg 19686 znadd 19708 tngplusg 22256 ttgplusg 25558 resvplusg 29164 hlhilsplus 36250 mendplusgfval 36774