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

Definition df-plusg 14234
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 14221 . 2  class  +g
2 c2 10359 . . 3  class  2
32cslot 14156 . 2  class Slot  2
41, 3wceq 1362 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  14255  plusgid  14256  grpstr  14260  grpbase  14261  grpplusg  14262  ressplusg  14263  frmdplusg  15512  oppradd  16656  sraaddg  17182  opsrplusg  17493  ply1plusgfvi  17595  zlmplusg  17792  znadd  17815  tngplusg  20070  ttgplusg  22947  resvplusg  26155  mendplusgfval  29387  hlhilsplus  35182
  Copyright terms: Public domain W3C validator