Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > df-plusg | Structured version Unicode version | |
| Description: Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| Ref | Expression |
|---|---|
| df-plusg |
   Slot  |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cplusg 14230 |
. 2
 | |
| 2 | c2 10363 |
. . 3
| |
| 3 | 2 | cslot 14165 |
. 2
Slot |
| 4 | 1, 3 | wceq 1369 |
1
 Slot |
| 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 |