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

Definition df-gid 23358
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 23353 . 2
2 vg . . 3
3 cvv 2951 . . 3
4 vu . . . . . . . . 9
54cv 1686 . . . . . . . 8
6 vx . . . . . . . . 9
76cv 1686 . . . . . . . 8
82cv 1686 . . . . . . . 8
95, 7, 8co 6061 . . . . . . 7
109, 7wceq 1687 . . . . . 6
117, 5, 8co 6061 . . . . . . 7
1211, 7wceq 1687 . . . . . 6
1310, 12wa 362 . . . . 5
148crn 4812 . . . . 5
1513, 6, 14wral 2694 . . . 4
1615, 4, 14crio 6019 . . 3
172, 3, 16cmpt 4325 . 2
181, 17wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  gidval  23379  fngid  23380
  Copyright terms: Public domain W3C validator