Definition df-exid

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cexid	|- ExId
1		vg	|- g
2		vx	|- x
3	1	cv	|- g
4	3	cdm	|- dom g
5	4	cdm	|- dom dom g
6		vy	|- y
7	2	cv	|- x
8	6	cv	|- y
9	7 8 3	co	|- ( x g y )
10	9 8	wceq	|- ( x g y ) = y
11	8 7 3	co	|- ( y g x )
12	11 8	wceq	|- ( y g x ) = y
13	10 12	wa	|- ( ( x g y ) = y /\ ( y g x ) = y )
14	13 6 5	wral	|- A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y )
15	14 2 5	wrex	|- E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y )
16	15 1	cab	|- { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }
17	0 16	wceq	|- ExId = { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }