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

Definition df-plusg 14587
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 14574 . 2  class  +g
2 c2 10591 . . 3  class  2
32cslot 14508 . 2  class Slot  2
41, 3wceq 1383 1  wff  +g  = Slot  2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  14608  plusgid  14609  grpstr  14613  grpbase  14614  grpplusg  14615  ressplusg  14616  frmdplusg  15896  oppradd  17153  sraaddg  17699  opsrplusg  18018  ply1plusgfvi  18157  zlmplusg  18429  znadd  18452  tngplusg  21029  ttgplusg  24053  resvplusg  27696  mendplusgfval  31110  hlhilsplus  37410
  Copyright terms: Public domain W3C validator