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

Definition df-plusg 14715
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 14702 . 2  class  +g
2 c2 10502 . . 3  class  2
32cslot 14633 . 2  class Slot  2
41, 3wceq 1399 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  14736  plusgid  14737  grpstr  14745  grpbase  14746  grpplusg  14747  ressplusg  14748  frmdplusg  16139  oppradd  17392  sraaddg  17938  opsrplusg  18257  ply1plusgfvi  18396  zlmplusg  18649  znadd  18670  tngplusg  21241  ttgplusg  24302  resvplusg  27977  mendplusgfval  31302  hlhilsplus  38083
  Copyright terms: Public domain W3C validator