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

Definition df-plusg 14568
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 14555 . 2  class  +g
2 c2 10585 . . 3  class  2
32cslot 14489 . 2  class Slot  2
41, 3wceq 1379 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  14589  plusgid  14590  grpstr  14594  grpbase  14595  grpplusg  14596  ressplusg  14597  frmdplusg  15854  oppradd  17080  sraaddg  17625  opsrplusg  17943  ply1plusgfvi  18082  zlmplusg  18351  znadd  18374  tngplusg  20919  ttgplusg  23885  resvplusg  27514  mendplusgfval  30767  hlhilsplus  36758
  Copyright terms: Public domain W3C validator