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 16568
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 16555 . 2 class +g
2 c2 11681 . . 3 class 2
32cslot 16472 . 2 class Slot 2
41, 3wceq 1528 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  16585  plusgid  16586  grpstr  16599  grpbase  16600  grpplusg  16601  ressplusg  16602  frmdplusg  18009  oppradd  19311  sraaddg  19882  opsrplusg  20190  ply1plusgfvi  20340  zlmplusg  20596  znadd  20617  tngplusg  23180  ttgplusg  26592  resvplusg  30834  hlhilsplus  38958  mendplusgfval  39665
  Copyright terms: Public domain W3C validator