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 17138
Description: Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form plusgid 17152 instead. (New usage is discouraged.)
Assertion
Ref Expression
df-plusg +g = Slot 2

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 17125 . 2 class +g
2 c2 12204 . . 3 class 2
32cslot 17045 . 2 class Slot 2
41, 3wceq 1541 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17151  plusgid  17152  grpstr  17157  grpbaseOLD  17160  grpplusgOLD  17162  oppraddOLD  20044  sraaddgOLD  20628  zlmplusgOLD  20907  znaddOLD  20931  opsrplusgOLD  21439  tngplusgOLD  23985  ttgplusgOLD  27710  resvplusgOLD  32010  hlhilsplusOLD  40373  mnringaddgdOLD  42440
  Copyright terms: Public domain W3C validator