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

Definition df-plusg 15165
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 15152 . 2  class  +g
2 c2 10659 . . 3  class  2
32cslot 15083 . 2  class Slot  2
41, 3wceq 1437 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  15186  plusgid  15187  grpstr  15195  grpbase  15196  grpplusg  15197  ressplusg  15198  frmdplusg  16589  oppradd  17793  sraaddg  18337  opsrplusg  18638  ply1plusgfvi  18770  zlmplusg  19021  znadd  19042  tngplusg  21581  ttgplusg  24754  resvplusg  28435  hlhilsplus  35219  mendplusgfval  35749
  Copyright terms: Public domain W3C validator