MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-0g Unicode version

Definition df-0g 14372
Description: Define group identity element. (Contributed by NM, 20-Aug-2011.)
Assertion
Ref Expression
df-0g
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-0g
StepHypRef Expression
1 c0g 14370 . 2
2 vg . . 3
3 cvv 2967 . . 3
4 ve . . . . . . 7
54cv 1368 . . . . . 6
62cv 1368 . . . . . . 7
7 cbs 14166 . . . . . . 7
86, 7cfv 5413 . . . . . 6
95, 8wcel 1756 . . . . 5
10 vx . . . . . . . . . 10
1110cv 1368 . . . . . . . . 9
12 cplusg 14230 . . . . . . . . . 10
136, 12cfv 5413 . . . . . . . . 9
145, 11, 13co 6086 . . . . . . . 8
1514, 11wceq 1369 . . . . . . 7
1611, 5, 13co 6086 . . . . . . . 8
1716, 11wceq 1369 . . . . . . 7
1815, 17wa 369 . . . . . 6
1918, 10, 8wral 2710 . . . . 5
209, 19wa 369 . . . 4
2120, 4cio 5374 . . 3
222, 3, 21cmpt 4345 . 2
231, 22wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  grpidval  15424  fn0g  15425
  Copyright terms: Public domain W3C validator