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

Definition df-plusg 13221
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 13208 . 2  class  +g
2 c2 9795 . . 3  class  2
32cslot 13147 . 2  class Slot  2
41, 3wceq 1623 1  wff  +g  = Slot  2
Colors of variables: wff set class
This definition is referenced by:  plusgndx  13242  plusgid  13243  grpstr  13247  grpbase  13248  grpplusg  13249  ressplusg  13250  frmdplusg  14476  oppradd  15412  sraaddg  15932  opsrplusg  16221  ply1plusgfvi  16320  zlmplusg  16473  znadd  16494  tngplusg  18158  mendplusgfval  27493  hlhilsplus  32133
  Copyright terms: Public domain W3C validator