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

Definition df-plusg 15258
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 15245 . 2  class  +g
2 c2 10692 . . 3  class  2
32cslot 15175 . 2  class Slot  2
41, 3wceq 1455 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  15279  plusgid  15280  grpstr  15291  grpbase  15292  grpplusg  15293  ressplusg  15294  frmdplusg  16693  oppradd  17913  sraaddg  18457  opsrplusg  18758  ply1plusgfvi  18890  zlmplusg  19145  znadd  19166  tngplusg  21705  ttgplusg  24964  resvplusg  28647  hlhilsplus  35557  mendplusgfval  36097
  Copyright terms: Public domain W3C validator