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

Definition df-plusg 16173
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
StepHypRef Expression
1 cplusg 16160 . 2 class +g
2 c2 11363 . . 3 class 2
32cslot 16074 . 2 class Slot 2
41, 3wceq 1637 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  16194  plusgid  16195  grpstr  16208  grpbase  16209  grpplusg  16210  ressplusg  16211  frmdplusg  17603  oppradd  18839  sraaddg  19395  opsrplusg  19695  ply1plusgfvi  19827  zlmplusg  20082  znadd  20103  tngplusg  22667  ttgplusg  25982  resvplusg  30168  hlhilsplus  37726  mendplusgfval  38261
  Copyright terms: Public domain W3C validator