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 14574 |
. 2
 | |
| 2 | c2 10591 |
. . 3
| |
| 3 | 2 | cslot 14508 |
. 2
Slot |
| 4 | 1, 3 | wceq 1383 |
1
 Slot |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 14608 plusgid 14609 grpstr 14613 grpbase 14614 grpplusg 14615 ressplusg 14616 frmdplusg 15896 oppradd 17153 sraaddg 17699 opsrplusg 18018 ply1plusgfvi 18157 zlmplusg 18429 znadd 18452 tngplusg 21029 ttgplusg 24053 resvplusg 27696 mendplusgfval 31110 hlhilsplus 37410 |
| Copyright terms: Public domain | W3C validator |