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 = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}

Distinct variable group:   𝑥,𝑔,𝑦

Detailed syntax breakdown of Definition df-exid

Step	Hyp	Ref	Expression
1		cexid 33643	. 2 class ExId
2		vx	. . . . . . . . 9 setvar 𝑥
3	2	cv 1482	. . . . . . . 8 class 𝑥
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1482	. . . . . . . 8 class 𝑦
6		vg	. . . . . . . . 9 setvar 𝑔
7	6	cv 1482	. . . . . . . 8 class 𝑔
8	3, 5, 7	co 6650	. . . . . . 7 class (𝑥𝑔𝑦)
9	8, 5	wceq 1483	. . . . . 6 wff (𝑥𝑔𝑦) = 𝑦
10	5, 3, 7	co 6650	. . . . . . 7 class (𝑦𝑔𝑥)
11	10, 5	wceq 1483	. . . . . 6 wff (𝑦𝑔𝑥) = 𝑦
12	9, 11	wa 384	. . . . 5 wff ((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
13	7	cdm 5114	. . . . . 6 class dom 𝑔
14	13	cdm 5114	. . . . 5 class dom dom 𝑔
15	12, 4, 14	wral 2912	. . . 4 wff ∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
16	15, 2, 14	wrex 2913	. . 3 wff ∃𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
17	16, 6	cab 2608	. 2 class {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
18	1, 17	wceq 1483	1 wff ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}

This definition is referenced by:  isexid  33646