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

Definition df-plusg 13497
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 13484 . 2  class  +g
2 c2 10005 . . 3  class  2
32cslot 13423 . 2  class Slot  2
41, 3wceq 1649 1  wff  +g  = Slot  2
Colors of variables: wff set class
This definition is referenced by:  plusgndx  13518  plusgid  13519  grpstr  13523  grpbase  13524  grpplusg  13525  ressplusg  13526  frmdplusg  14754  oppradd  15690  sraaddg  16206  opsrplusg  16495  ply1plusgfvi  16591  zlmplusg  16755  znadd  16776  tngplusg  18636  mendplusgfval  27361  hlhilsplus  32426
  Copyright terms: Public domain W3C validator