Definition df-exid 10362

Description: A device to add an identity element to various sorts of internal operations.

Assertion

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

Distinct variable group:   x,g,y

Detailed syntax breakdown of Definition df-exid

Step	Hyp	Ref	Expression
1		cexid 10361	. 2 class ExId
2		vy	. . . . . . . . 9 set y
3	2	cv 1297	. . . . . . . 8 class y
4		vx	. . . . . . . . 9 set x
5	4	cv 1297	. . . . . . . 8 class x
6		vg	. . . . . . . . 9 set g
7	6	cv 1297	. . . . . . . 8 class g
8	3, 5, 7	co 4884	. . . . . . 7 class (ygx)
9	8, 3	wceq 1298	. . . . . 6 wff (ygx) = y
10	5, 3, 7	co 4884	. . . . . . 7 class (xgy)
11	10, 3	wceq 1298	. . . . . 6 wff (xgy) = y
12	9, 11	wa 240	. . . . 5 wff ((ygx) = y /\ (xgy) = y)
13	7	cdm 3986	. . . . . 6 class dom g
14	13	cdm 3986	. . . . 5 class dom dom g
15	12, 2, 14	wral 2105	. . . 4 wff A.y e. dom dom g((ygx) = y /\ (xgy) = y)
16	15, 4, 14	wrex 2106	. . 3 wff E.x e. dom dom gA.y e. dom dom g((ygx) = y /\ (xgy) = y)
17	16, 6	cab 1871	. 2 class {g | E.x e. dom dom gA.y e. dom dom g((ygx) = y /\ (xgy) = y)}
18	1, 17	wceq 1298	1 wff ExId = {g | E.x e. dom dom gA.y e. dom dom g((ygx) = y /\ (xgy) = y)}

This definition is referenced by:  isexid 10364

Copyright terms: Public domain