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

Definition df-plusg 16815
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 16802 . 2 class +g
2 c2 11885 . . 3 class 2
32cslot 16734 . 2 class Slot 2
41, 3wceq 1543 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  16828  plusgid  16829  grpstr  16831  grpbase  16832  grpplusg  16833  frmdplusg  18281  oppradd  19648  sraaddg  20216  zlmplusg  20485  znadd  20505  opsrplusg  21008  ply1plusgfvi  21163  tngplusg  23540  ttgplusg  26969  resvplusg  31251  bj-endcomp  35222  hlhilsplus  39691  mendplusgfval  40713  mnringaddgd  41511
  Copyright terms: Public domain W3C validator