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

Definition df-plusg 14243
Description: Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-plusg

Detailed syntax breakdown of Definition df-plusg
StepHypRef Expression
1 cplusg 14230 . 2
2 c2 10363 . . 3
32cslot 14165 . 2
41, 3wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  plusgndx  14264  plusgid  14265  grpstr  14269  grpbase  14270  grpplusg  14271  ressplusg  14272  frmdplusg  15523  oppradd  16712  sraaddg  17240  opsrplusg  17541  ply1plusgfvi  17677  zlmplusg  17930  znadd  17953  tngplusg  20208  ttgplusg  23092  resvplusg  26270  mendplusgfval  29513  hlhilsplus  35481
  Copyright terms: Public domain W3C validator