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

Definition df-gid 21781
 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 GId
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-gid
StepHypRef Expression
1 cgi 21776 . 2 GId
2 vg . . 3
3 cvv 2957 . . 3
4 vu . . . . . . . . 9
54cv 1652 . . . . . . . 8
6 vx . . . . . . . . 9
76cv 1652 . . . . . . . 8
82cv 1652 . . . . . . . 8
95, 7, 8co 6082 . . . . . . 7
109, 7wceq 1653 . . . . . 6
117, 5, 8co 6082 . . . . . . 7
1211, 7wceq 1653 . . . . . 6
1310, 12wa 360 . . . . 5
148crn 4880 . . . . 5
1513, 6, 14wral 2706 . . . 4
1615, 4, 14crio 6543 . . 3
172, 3, 16cmpt 4267 . 2
181, 17wceq 1653 1 GId
 Colors of variables: wff set class This definition is referenced by:  gidval  21802  fngid  21803
 Copyright terms: Public domain W3C validator