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 15948
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 15935 . 2 class +g
2 c2 11067 . . 3 class 2
32cslot 15850 . 2 class Slot 2
41, 3wceq 1482 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  15970  plusgid  15971  grpstr  15984  grpbase  15985  grpplusg  15986  ressplusg  15987  frmdplusg  17385  oppradd  18624  sraaddg  19173  opsrplusg  19474  ply1plusgfvi  19606  zlmplusg  19861  znadd  19883  tngplusg  22440  ttgplusg  25752  resvplusg  29818  hlhilsplus  37058  mendplusgfval  37581
  Copyright terms: Public domain W3C validator