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 16395

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 16382	. 2 class +_g
2		c2 11529	. . 3 class 2
3	2	cslot 16299	. 2 class Slot 2
4	1, 3	wceq 1520	1 wff +_g = Slot 2

Colors of variables: wff setvar class

This definition is referenced by: plusgndx 16412 plusgid 16413 grpstr 16426 grpbase 16427 grpplusg 16428 ressplusg 16429 frmdplusg 17818 oppradd 19058 sraaddg 19629 opsrplusg 19935 ply1plusgfvi 20081 zlmplusg 20336 znadd 20357 tngplusg 22922 ttgplusg 26335 resvplusg 30515 hlhilsplus 38557 mendplusgfval 39221