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 16565 | . 2 class +g | |
| 2 | c2 11693 | . . 3 class 2 | |
| 3 | 2 | cslot 16482 | . 2 class Slot 2 |
| 4 | 1, 3 | wceq 1537 | 1 wff +g = Slot 2 |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 16595 plusgid 16596 grpstr 16609 grpbase 16610 grpplusg 16611 ressplusg 16612 frmdplusg 18019 oppradd 19380 sraaddg 19951 opsrplusg 20260 ply1plusgfvi 20410 zlmplusg 20666 znadd 20687 tngplusg 23251 ttgplusg 26664 resvplusg 30906 bj-endcomp 34601 hlhilsplus 39091 mendplusgfval 39834 |
| Copyright terms: Public domain | W3C validator |