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

Definition df-plusg 13530
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 13517 . 2  class  +g
2 c2 10038 . . 3  class  2
32cslot 13456 . 2  class Slot  2
41, 3wceq 1652 1  wff  +g  = Slot  2
Colors of variables: wff set class
This definition is referenced by:  plusgndx  13551  plusgid  13552  grpstr  13556  grpbase  13557  grpplusg  13558  ressplusg  13559  frmdplusg  14787  oppradd  15723  sraaddg  16239  opsrplusg  16528  ply1plusgfvi  16624  zlmplusg  16788  znadd  16809  tngplusg  18671  mendplusgfval  27408  hlhilsplus  32580
  Copyright terms: Public domain W3C validator