Definition df-ssetk 4194

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

Assertion

Ref	Expression
df-ssetk	⊢ Sk = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y ⊆ z)}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-ssetk

Step	Hyp	Ref	Expression
1		cssetk 4184	. 2 class Sk
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	5, 7	wss 3258	. . . . . 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 Sk = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ y ⊆ z)}

This definition is referenced by:  opkelssetkg  4269  ssetkssvvk  4279