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

Definition df-plusg 13544
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 13531 . 2  class  +g
2 c2 10051 . . 3  class  2
32cslot 13470 . 2  class Slot  2
41, 3wceq 1653 1  wff  +g  = Slot  2
Colors of variables: wff set class
This definition is referenced by:  plusgndx  13565  plusgid  13566  grpstr  13570  grpbase  13571  grpplusg  13572  ressplusg  13573  frmdplusg  14801  oppradd  15737  sraaddg  16253  opsrplusg  16542  ply1plusgfvi  16638  zlmplusg  16802  znadd  16823  tngplusg  18685  mendplusgfval  27472  hlhilsplus  32803
  Copyright terms: Public domain W3C validator