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 15723
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 15710 . 2 class +g
2 c2 10913 . . 3 class 2
32cslot 15636 . 2 class Slot 2
41, 3wceq 1474 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  15745  plusgid  15746  grpstr  15757  grpbase  15758  grpplusg  15759  ressplusg  15760  frmdplusg  17156  oppradd  18395  sraaddg  18942  opsrplusg  19243  ply1plusgfvi  19375  zlmplusg  19627  znadd  19649  tngplusg  22190  ttgplusg  25472  resvplusg  28966  hlhilsplus  36049  mendplusgfval  36573
  Copyright terms: Public domain W3C validator