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 14221 |
. 2
 | |
| 2 | c2 10359 |
. . 3
| |
| 3 | 2 | cslot 14156 |
. 2
Slot |
| 4 | 1, 3 | wceq 1362 |
1
 Slot |
| Colors of variables: wff setvar class |
| This definition is referenced by: plusgndx 14255 plusgid 14256 grpstr 14260 grpbase 14261 grpplusg 14262 ressplusg 14263 frmdplusg 15512 oppradd 16656 sraaddg 17182 opsrplusg 17493 ply1plusgfvi 17595 zlmplusg 17792 znadd 17815 tngplusg 20070 ttgplusg 22947 resvplusg 26155 mendplusgfval 29387 hlhilsplus 35182 |
| Copyright terms: Public domain | W3C validator |