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

Definition df-gid 24148
Description: Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
df-gid
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-gid
StepHypRef Expression
1 cgi 24143 . 2
2 vg . . 3
3 cvv 3081 . . 3
4 vu . . . . . . . . 9
54cv 1369 . . . . . . . 8
6 vx . . . . . . . . 9
76cv 1369 . . . . . . . 8
82cv 1369 . . . . . . . 8
95, 7, 8co 6222 . . . . . . 7
109, 7wceq 1370 . . . . . 6
117, 5, 8co 6222 . . . . . . 7
1211, 7wceq 1370 . . . . . 6
1310, 12wa 369 . . . . 5
148crn 4958 . . . . 5
1513, 6, 14wral 2800 . . . 4
1615, 4, 14crio 6182 . . 3
172, 3, 16cmpt 4467 . 2
181, 17wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  gidval  24169  fngid  24170
  Copyright terms: Public domain W3C validator