Definition df-cnvk 4187

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

Assertion

Ref	Expression
df-cnvk	|- `'kA = {x | E.yE.z(x = <<y, z>> /\ <<z, y>> e. A)}

Distinct variable group:   x,A,y,z

Detailed syntax breakdown of Definition df-cnvk

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	ccnvk 4176	. 2 class `'kA
3		vx	. . . . . . . 8 setvar x
4	3	cv 1641	. . . . . . 7 class x
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1641	. . . . . . . 8 class y
7		vz	. . . . . . . . 9 setvar z
8	7	cv 1641	. . . . . . . 8 class z
9	6, 8	copk 4058	. . . . . . 7 class <<y, z>>
10	4, 9	wceq 1642	. . . . . 6 wff x = <<y, z>>
11	8, 6	copk 4058	. . . . . . 7 class <<z, y>>
12	11, 1	wcel 1710	. . . . . 6 wff <<z, y>> e. A
13	10, 12	wa 358	. . . . 5 wff (x = <<y, z>> /\ <<z, y>> e. A)
14	13, 7	wex 1541	. . . 4 wff E.z(x = <<y, z>> /\ <<z, y>> e. A)
15	14, 5	wex 1541	. . 3 wff E.yE.z(x = <<y, z>> /\ <<z, y>> e. A)
16	15, 3	cab 2339	. 2 class {x | E.yE.z(x = <<y, z>> /\ <<z, y>> e. A)}
17	2, 16	wceq 1642	1 wff `'kA = {x | E.yE.z(x = <<y, z>> /\ <<z, y>> e. A)}

This definition is referenced by:  cnvkeq  4216  opkelcnvkg  4250  cnvkssvvk  4276