Definition df-gid 24870

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 24865	. 2 class GId
2		vg	. . 3 setvar g
3		cvv 3113	. . 3 class _V
4		vu	. . . . . . . . 9 setvar u
5	4	cv 1378	. . . . . . . 8 class u
6		vx	. . . . . . . . 9 setvar x
7	6	cv 1378	. . . . . . . 8 class x
8	2	cv 1378	. . . . . . . 8 class g
9	5, 7, 8	co 6282	. . . . . . 7 class ( u g x )
10	9, 7	wceq 1379	. . . . . 6 wff ( u g x ) = x
11	7, 5, 8	co 6282	. . . . . . 7 class ( x g u )
12	11, 7	wceq 1379	. . . . . 6 wff ( x g u ) = x
13	10, 12	wa 369	. . . . 5 wff ( ( u g x ) = x /\ ( x g u ) = x )
14	8	crn 5000	. . . . 5 class ran g
15	13, 6, 14	wral 2814	. . . 4 wff A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x )
16	15, 4, 14	crio 6242	. . 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 4505	. 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 1379	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  24891  fngid  24892