Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-0g Unicode version

Definition df-0g 12149
 Description: Define group identity element. Remark: this definition is required here because the symbol is already used in df-gsum 12150. The related theorems will be provided later. (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 12147 . 2
2 vg . . 3
3 cvv 2686 . . 3
4 ve . . . . . . 7
54cv 1330 . . . . . 6
62cv 1330 . . . . . . 7
7 cbs 11969 . . . . . . 7
86, 7cfv 5123 . . . . . 6
95, 8wcel 1480 . . . . 5
10 vx . . . . . . . . . 10
1110cv 1330 . . . . . . . . 9
12 cplusg 12031 . . . . . . . . . 10
136, 12cfv 5123 . . . . . . . . 9
145, 11, 13co 5774 . . . . . . . 8
1514, 11wceq 1331 . . . . . . 7
1611, 5, 13co 5774 . . . . . . . 8
1716, 11wceq 1331 . . . . . . 7
1815, 17wa 103 . . . . . 6
1918, 10, 8wral 2416 . . . . 5
209, 19wa 103 . . . 4
2120, 4cio 5086 . . 3
222, 3, 21cmpt 3989 . 2
231, 22wceq 1331 1
 Colors of variables: wff set class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator