Definition df-exid 33644

Description: A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)

Assertion

Ref	Expression
df-exid	|- ExId = { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }

Distinct variable group:   x, g, y

Detailed syntax breakdown of Definition df-exid

Step	Hyp	Ref	Expression
1		cexid 33643	. 2 class ExId
2		vx	. . . . . . . . 9 setvar x
3	2	cv 1482	. . . . . . . 8 class x
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1482	. . . . . . . 8 class y
6		vg	. . . . . . . . 9 setvar g
7	6	cv 1482	. . . . . . . 8 class g
8	3, 5, 7	co 6650	. . . . . . 7 class ( x g y )
9	8, 5	wceq 1483	. . . . . 6 wff ( x g y ) = y
10	5, 3, 7	co 6650	. . . . . . 7 class ( y g x )
11	10, 5	wceq 1483	. . . . . 6 wff ( y g x ) = y
12	9, 11	wa 384	. . . . 5 wff ( ( x g y ) = y /\ ( y g x ) = y )
13	7	cdm 5114	. . . . . 6 class dom g
14	13	cdm 5114	. . . . 5 class dom dom g
15	12, 4, 14	wral 2912	. . . 4 wff A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y )
16	15, 2, 14	wrex 2913	. . 3 wff E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y )
17	16, 6	cab 2608	. 2 class { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }
18	1, 17	wceq 1483	1 wff ExId = { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }

This definition is referenced by:  isexid  33646