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 14555 |
. 2
 | |
| 2 | c2 10585 |
. . 3
| |
| 3 | 2 | cslot 14489 |
. 2
Slot |
| 4 | 1, 3 | wceq 1379 |
1
 Slot |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 14589 plusgid 14590 grpstr 14594 grpbase 14595 grpplusg 14596 ressplusg 14597 frmdplusg 15854 oppradd 17080 sraaddg 17625 opsrplusg 17943 ply1plusgfvi 18082 zlmplusg 18351 znadd 18374 tngplusg 20919 ttgplusg 23885 resvplusg 27514 mendplusgfval 30767 hlhilsplus 36758 |
| Copyright terms: Public domain | W3C validator |