Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > df-plusg | Structured version Visualization 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 15245 |
. 2
 | |
| 2 | c2 10692 |
. . 3
| |
| 3 | 2 | cslot 15175 |
. 2
Slot |
| 4 | 1, 3 | wceq 1455 |
1
 Slot |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 15279 plusgid 15280 grpstr 15291 grpbase 15292 grpplusg 15293 ressplusg 15294 frmdplusg 16693 oppradd 17913 sraaddg 18457 opsrplusg 18758 ply1plusgfvi 18890 zlmplusg 19145 znadd 19166 tngplusg 21705 ttgplusg 24964 resvplusg 28647 hlhilsplus 35557 mendplusgfval 36097 |
| Copyright terms: Public domain | W3C validator |