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

Definition df-plusg 15202
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 15189 . 2  class  +g
2 c2 10666 . . 3  class  2
32cslot 15119 . 2  class Slot  2
41, 3wceq 1437 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  15223  plusgid  15224  grpstr  15235  grpbase  15236  grpplusg  15237  ressplusg  15238  frmdplusg  16637  oppradd  17857  sraaddg  18401  opsrplusg  18702  ply1plusgfvi  18834  zlmplusg  19088  znadd  19109  tngplusg  21648  ttgplusg  24906  resvplusg  28604  hlhilsplus  35480  mendplusgfval  36021
  Copyright terms: Public domain W3C validator