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 14702 |
. 2
 | |
| 2 | c2 10502 |
. . 3
| |
| 3 | 2 | cslot 14633 |
. 2
Slot |
| 4 | 1, 3 | wceq 1399 |
1
 Slot |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 14736 plusgid 14737 grpstr 14745 grpbase 14746 grpplusg 14747 ressplusg 14748 frmdplusg 16139 oppradd 17392 sraaddg 17938 opsrplusg 18257 ply1plusgfvi 18396 zlmplusg 18649 znadd 18670 tngplusg 21241 ttgplusg 24302 resvplusg 27977 mendplusgfval 31302 hlhilsplus 38083 |
| Copyright terms: Public domain | W3C validator |