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

Definition df-0g 13729
 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 13725 . 2
2 vg . . 3
3 cvv 2958 . . 3
4 ve . . . . . . 7
54cv 1652 . . . . . 6
62cv 1652 . . . . . . 7
7 cbs 13471 . . . . . . 7
86, 7cfv 5456 . . . . . 6
95, 8wcel 1726 . . . . 5
10 vx . . . . . . . . . 10
1110cv 1652 . . . . . . . . 9
12 cplusg 13531 . . . . . . . . . 10
136, 12cfv 5456 . . . . . . . . 9
145, 11, 13co 6083 . . . . . . . 8
1514, 11wceq 1653 . . . . . . 7
1611, 5, 13co 6083 . . . . . . . 8
1716, 11wceq 1653 . . . . . . 7
1815, 17wa 360 . . . . . 6
1918, 10, 8wral 2707 . . . . 5
209, 19wa 360 . . . 4
2120, 4cio 5418 . . 3
222, 3, 21cmpt 4268 . 2
231, 22wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  grpidval  14709  fn0g  14710
 Copyright terms: Public domain W3C validator