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

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 16971 . 2 class +g
2 c2 12037 . . 3 class 2
32cslot 16891 . 2 class Slot 2
41, 3wceq 1539 1 wff +g = Slot 2
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  16997  plusgid  16998  grpstr  17003  grpbaseOLD  17006  grpplusgOLD  17008  oppraddOLD  19881  sraaddgOLD  20453  zlmplusgOLD  20732  znaddOLD  20756  opsrplusgOLD  21264  tngplusgOLD  23810  ttgplusgOLD  27252  resvplusgOLD  31544  hlhilsplusOLD  39964  mnringaddgdOLD  41843
  Copyright terms: Public domain W3C validator