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

Definition df-plusg 14369
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 14356 . 2  class  +g
2 c2 10481 . . 3  class  2
32cslot 14290 . 2  class Slot  2
41, 3wceq 1370 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  14390  plusgid  14391  grpstr  14395  grpbase  14396  grpplusg  14397  ressplusg  14398  frmdplusg  15650  oppradd  16844  sraaddg  17382  opsrplusg  17684  ply1plusgfvi  17819  zlmplusg  18074  znadd  18097  tngplusg  20359  ttgplusg  23275  resvplusg  26445  mendplusgfval  29689  hlhilsplus  35911
  Copyright terms: Public domain W3C validator