Definition df-ssetk 4194

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

Assertion

Ref	Expression
df-ssetk	|- Sk = {x | E.yE.z(x = <<y, z>> /\ y C_ 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 C_ z
11	9, 10	wa 358	. . . . 5 wff (x = <<y, z>> /\ y C_ z)
12	11, 6	wex 1541	. . . 4 wff E.z(x = <<y, z>> /\ y C_ z)
13	12, 4	wex 1541	. . 3 wff E.yE.z(x = <<y, z>> /\ y C_ z)
14	13, 2	cab 2339	. 2 class {x | E.yE.z(x = <<y, z>> /\ y C_ z)}
15	1, 14	wceq 1642	1 wff Sk = {x | E.yE.z(x = <<y, z>> /\ y C_ z)}

This definition is referenced by:  opkelssetkg  4269  ssetkssvvk  4279