Axiom ax-si 4084

Description: State the axiom of the singleton image. This axiom guarantees that guarantees the existence of a set that raises the "type" of another set when considered as a relationship. Axiom P2 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-si	|- E.yA.zA.w(<<{z}, {w}>> e. y <-> <<z, w>> e. x)

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-si

Step	Hyp	Ref	Expression
1		vz	. . . . . . . . 9 setvar z
2	1	cv 1641	. . . . . . . 8 class z
3	2	csn 3738	. . . . . . 7 class {z}
4		vw	. . . . . . . . 9 setvar w
5	4	cv 1641	. . . . . . . 8 class w
6	5	csn 3738	. . . . . . 7 class {w}
7	3, 6	copk 4058	. . . . . 6 class <<{z}, {w}>>
8		vy	. . . . . . 7 setvar y
9	8	cv 1641	. . . . . 6 class y
10	7, 9	wcel 1710	. . . . 5 wff <<{z}, {w}>> e. y
11	2, 5	copk 4058	. . . . . 6 class <<z, w>>
12		vx	. . . . . . 7 setvar x
13	12	cv 1641	. . . . . 6 class x
14	11, 13	wcel 1710	. . . . 5 wff <<z, w>> e. x
15	10, 14	wb 176	. . . 4 wff (<<{z}, {w}>> e. y <-> <<z, w>> e. x)
16	15, 4	wal 1540	. . 3 wff A.w(<<{z}, {w}>> e. y <-> <<z, w>> e. x)
17	16, 1	wal 1540	. 2 wff A.zA.w(<<{z}, {w}>> e. y <-> <<z, w>> e. x)
18	17, 8	wex 1541	1 wff E.yA.zA.w(<<{z}, {w}>> e. y <-> <<z, w>> e. x)

This axiom is referenced by:  axsiprim  4094  sikexg  4297