Axiom ax-cnv 4081

Description: State the axiom of converse. This axiom guarantees the existence of the Kuratowski converse of x. Axiom P7 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-cnv	⊢ ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-cnv

Step	Hyp	Ref	Expression
1		vz	. . . . . . . 8 setvar z
2	1	cv 1641	. . . . . . 7 class z
3		vw	. . . . . . . 8 setvar w
4	3	cv 1641	. . . . . . 7 class w
5	2, 4	copk 4058	. . . . . 6 class ⟪z, w⟫
6		vy	. . . . . . 7 setvar y
7	6	cv 1641	. . . . . 6 class y
8	5, 7	wcel 1710	. . . . 5 wff ⟪z, w⟫ ∈ y
9	4, 2	copk 4058	. . . . . 6 class ⟪w, z⟫
10		vx	. . . . . . 7 setvar x
11	10	cv 1641	. . . . . 6 class x
12	9, 11	wcel 1710	. . . . 5 wff ⟪w, z⟫ ∈ x
13	8, 12	wb 176	. . . 4 wff (⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)
14	13, 3	wal 1540	. . 3 wff ∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)
15	14, 1	wal 1540	. 2 wff ∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)
16	15, 6	wex 1541	1 wff ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)

This axiom is referenced by:  axcnvprim  4092  cnvkexg  4287