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

Definition df-plusg 13216
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 13203 . 2  class  +g
2 c2 9791 . . 3  class  2
32cslot 13142 . 2  class Slot  2
41, 3wceq 1624 1  wff  +g  = Slot  2
Colors of variables: wff set class
This definition is referenced by:  plusgndx  13237  plusgid  13238  grpstr  13242  grpbase  13243  grpplusg  13244  ressplusg  13245  frmdplusg  14471  oppradd  15407  sraaddg  15927  opsrplusg  16216  ply1plusgfvi  16315  zlmplusg  16468  znadd  16489  tngplusg  18153  mendplusgfval  26893  hlhilsplus  31401
  Copyright terms: Public domain W3C validator