Definition df-gid 21733

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 = ( g e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )

Distinct variable group:   u, g, x

Detailed syntax breakdown of Definition df-gid

Step	Hyp	Ref	Expression
1		cgi 21728	. 2 class GId
2		vg	. . 3 set g
3		cvv 2916	. . 3 class _V
4		vu	. . . . . . . . 9 set u
5	4	cv 1648	. . . . . . . 8 class u
6		vx	. . . . . . . . 9 set x
7	6	cv 1648	. . . . . . . 8 class x
8	2	cv 1648	. . . . . . . 8 class g
9	5, 7, 8	co 6040	. . . . . . 7 class ( u g x )
10	9, 7	wceq 1649	. . . . . 6 wff ( u g x ) = x
11	7, 5, 8	co 6040	. . . . . . 7 class ( x g u )
12	11, 7	wceq 1649	. . . . . 6 wff ( x g u ) = x
13	10, 12	wa 359	. . . . 5 wff ( ( u g x ) = x /\ ( x g u ) = x )
14	8	crn 4838	. . . . 5 class ran g
15	13, 6, 14	wral 2666	. . . 4 wff A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x )
16	15, 4, 14	crio 6501	. . 3 class ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) )
17	2, 3, 16	cmpt 4226	. 2 class ( g e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )
18	1, 17	wceq 1649	1 wff GId = ( g e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )

This definition is referenced by:  gidval  21754  fngid  21755