Definition df-idk 4196

Description: Define the Kuratowski identity relationship. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-idk	⊢ Ik = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y = z)}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-idk

Step	Hyp	Ref	Expression
1		cidk 4185	. 2 class Ik
2		vx	. . . . . . . 8 setvar x
3	2	cv 1641	. . . . . . 7 class x
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1641	. . . . . . . 8 class y
6		vz	. . . . . . . . 9 setvar z
7	6	cv 1641	. . . . . . . 8 class z
8	5, 7	copk 4058	. . . . . . 7 class ⟪y, z⟫
9	3, 8	wceq 1642	. . . . . 6 wff x = ⟪y, z⟫
10	4, 6	weq 1643	. . . . . 6 wff y = z
11	9, 10	wa 358	. . . . 5 wff (x = ⟪y, z⟫ ∧ y = z)
12	11, 6	wex 1541	. . . 4 wff ∃z(x = ⟪y, z⟫ ∧ y = z)
13	12, 4	wex 1541	. . 3 wff ∃y∃z(x = ⟪y, z⟫ ∧ y = z)
14	13, 2	cab 2339	. 2 class {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y = z)}
15	1, 14	wceq 1642	1 wff Ik = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y = z)}

This definition is referenced by:  opkelidkg  4275  idkssvvk  4282