Definition df-cnvk 4187

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

Assertion

Ref	Expression
df-cnvk	⊢ ◡kA = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ 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⟫ ∈ A
13	10, 12	wa 358	. . . . 5 wff (x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ A)
14	13, 7	wex 1541	. . . 4 wff ∃z(x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ A)
15	14, 5	wex 1541	. . 3 wff ∃y∃z(x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ A)
16	15, 3	cab 2339	. 2 class {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ A)}
17	2, 16	wceq 1642	1 wff ◡kA = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ⟪z, y⟫ ∈ A)}

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