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 16001
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 15988 . 2 class +g
2 c2 11108 . . 3 class 2
32cslot 15903 . 2 class Slot 2
41, 3wceq 1523 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  16023  plusgid  16024  grpstr  16037  grpbase  16038  grpplusg  16039  ressplusg  16040  frmdplusg  17438  oppradd  18676  sraaddg  19227  opsrplusg  19528  ply1plusgfvi  19660  zlmplusg  19915  znadd  19937  tngplusg  22493  ttgplusg  25803  resvplusg  29961  hlhilsplus  37549  mendplusgfval  38072
  Copyright terms: Public domain W3C validator