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	|- E.yA.zA.w(<<z, w>> e. y <-> <<w, z>> e. 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>> e. 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>> e. x
13	8, 12	wb 176	. . . 4 wff (<<z, w>> e. y <-> <<w, z>> e. x)
14	13, 3	wal 1540	. . 3 wff A.w(<<z, w>> e. y <-> <<w, z>> e. x)
15	14, 1	wal 1540	. 2 wff A.zA.w(<<z, w>> e. y <-> <<w, z>> e. x)
16	15, 6	wex 1541	1 wff E.yA.zA.w(<<z, w>> e. y <-> <<w, z>> e. x)

This axiom is referenced by:  axcnvprim  4092  cnvkexg  4287