Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-plusg | Structured version Visualization version GIF version |
Description: Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Ref | Expression |
---|---|
df-plusg | ⊢ +g = Slot 2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cplusg 16555 | . 2 class +g | |
2 | c2 11681 | . . 3 class 2 | |
3 | 2 | cslot 16472 | . 2 class Slot 2 |
4 | 1, 3 | wceq 1528 | 1 wff +g = Slot 2 |
Colors of variables: wff setvar class |
This definition is referenced by: plusgndx 16585 plusgid 16586 grpstr 16599 grpbase 16600 grpplusg 16601 ressplusg 16602 frmdplusg 18009 oppradd 19311 sraaddg 19882 opsrplusg 20190 ply1plusgfvi 20340 zlmplusg 20596 znadd 20617 tngplusg 23180 ttgplusg 26592 resvplusg 30834 hlhilsplus 38958 mendplusgfval 39665 |
Copyright terms: Public domain | W3C validator |