Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-plusg | Structured version Visualization version GIF version |
Description: Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Ref | Expression |
---|---|
df-plusg | ⊢ +g = Slot 2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cplusg 15768 | . 2 class +g | |
2 | c2 10947 | . . 3 class 2 | |
3 | 2 | cslot 15694 | . 2 class Slot 2 |
4 | 1, 3 | wceq 1475 | 1 wff +g = Slot 2 |
Colors of variables: wff setvar class |
This definition is referenced by: plusgndx 15803 plusgid 15804 grpstr 15815 grpbase 15816 grpplusg 15817 ressplusg 15818 frmdplusg 17214 oppradd 18453 sraaddg 19000 opsrplusg 19301 ply1plusgfvi 19433 zlmplusg 19686 znadd 19708 tngplusg 22256 ttgplusg 25558 resvplusg 29164 hlhilsplus 36250 mendplusgfval 36774 |
Copyright terms: Public domain | W3C validator |