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

Definition df-plusg 13312
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 13299 . 2  class  +g
2 c2 9882 . . 3  class  2
32cslot 13238 . 2  class Slot  2
41, 3wceq 1642 1  wff  +g  = Slot  2
Colors of variables: wff set class
This definition is referenced by:  plusgndx  13333  plusgid  13334  grpstr  13338  grpbase  13339  grpplusg  13340  ressplusg  13341  frmdplusg  14569  oppradd  15505  sraaddg  16025  opsrplusg  16314  ply1plusgfvi  16413  zlmplusg  16573  znadd  16594  tngplusg  18254  mendplusgfval  26816  hlhilsplus  32185
  Copyright terms: Public domain W3C validator