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 14356 |
. 2
 | |
| 2 | c2 10481 |
. . 3
| |
| 3 | 2 | cslot 14290 |
. 2
Slot |
| 4 | 1, 3 | wceq 1370 |
1
 Slot |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 14390 plusgid 14391 grpstr 14395 grpbase 14396 grpplusg 14397 ressplusg 14398 frmdplusg 15650 oppradd 16844 sraaddg 17382 opsrplusg 17684 ply1plusgfvi 17819 zlmplusg 18074 znadd 18097 tngplusg 20359 ttgplusg 23275 resvplusg 26445 mendplusgfval 29689 hlhilsplus 35911 |
| Copyright terms: Public domain | W3C validator |