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 15941 | . 2 class +g | |
| 2 | c2 11070 | . . 3 class 2 | |
| 3 | 2 | cslot 15856 | . 2 class Slot 2 |
| 4 | 1, 3 | wceq 1483 | 1 wff +g = Slot 2 |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 15976 plusgid 15977 grpstr 15990 grpbase 15991 grpplusg 15992 ressplusg 15993 frmdplusg 17391 oppradd 18630 sraaddg 19179 opsrplusg 19480 ply1plusgfvi 19612 zlmplusg 19867 znadd 19889 tngplusg 22446 ttgplusg 25758 resvplusg 29833 hlhilsplus 37232 mendplusgfval 37755 |
| Copyright terms: Public domain | W3C validator |