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

Definition df-0g 13682
 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 13678 . 2
2 vg . . 3
3 cvv 2916 . . 3
4 ve . . . . . . 7
54cv 1648 . . . . . 6
62cv 1648 . . . . . . 7
7 cbs 13424 . . . . . . 7
86, 7cfv 5413 . . . . . 6
95, 8wcel 1721 . . . . 5
10 vx . . . . . . . . . 10
1110cv 1648 . . . . . . . . 9
12 cplusg 13484 . . . . . . . . . 10
136, 12cfv 5413 . . . . . . . . 9
145, 11, 13co 6040 . . . . . . . 8
1514, 11wceq 1649 . . . . . . 7
1611, 5, 13co 6040 . . . . . . . 8
1716, 11wceq 1649 . . . . . . 7
1815, 17wa 359 . . . . . 6
1918, 10, 8wral 2666 . . . . 5
209, 19wa 359 . . . 4
2120, 4cio 5375 . . 3
222, 3, 21cmpt 4226 . 2
231, 22wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  grpidval  14662  fn0g  14663
 Copyright terms: Public domain W3C validator