Nearby theorems
|
|
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 16802 | . 2 class +g | |
| 2 | c2 11885 | . . 3 class 2 | |
| 3 | 2 | cslot 16734 | . 2 class Slot 2 |
| 4 | 1, 3 | wceq 1543 | 1 wff +g = Slot 2 |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 16828 plusgid 16829 grpstr 16831 grpbase 16832 grpplusg 16833 frmdplusg 18281 oppradd 19648 sraaddg 20216 zlmplusg 20485 znadd 20505 opsrplusg 21008 ply1plusgfvi 21163 tngplusg 23540 ttgplusg 26969 resvplusg 31251 bj-endcomp 35222 hlhilsplus 39691 mendplusgfval 40713 mnringaddgd 41511 |
| Copyright terms: Public domain | W3C validator |