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

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 17147 . 2 class +g
2 c2 12217 . . 3 class 2
32cslot 17064 . 2 class Slot 2
41, 3wceq 1541 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  17173  plusgid  17174  grpstr  17179  grpbaseOLD  17182  grpplusgOLD  17184  oppraddOLD  20073  sraaddgOLD  20702  zlmplusgOLD  20959  znaddOLD  20983  opsrplusgOLD  21492  tngplusgOLD  24038  ttgplusgOLD  27887  resvplusgOLD  32198  hlhilsplusOLD  40479  mnringaddgdOLD  42620
  Copyright terms: Public domain W3C validator