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	⊢ ∃y∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ 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}⟫ ∈ 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⟫ ∈ x
15	10, 14	wb 176	. . . 4 wff (⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
16	15, 4	wal 1540	. . 3 wff ∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
17	16, 1	wal 1540	. 2 wff ∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)
18	17, 8	wex 1541	1 wff ∃y∀z∀w(⟪{z}, {w}⟫ ∈ y ↔ ⟪z, w⟫ ∈ x)

This axiom is referenced by:  axsiprim  4094  sikexg  4297