Axiom ax-sn 4087

Description: The singleton axiom. This axiom sets up the existence of a singleton set. This appears to have been an oversight on Hailperin's part, as it is needed to prove the properties of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-sn	⊢ ∃y∀z(z ∈ y ↔ z = x)

Distinct variable group:   x,y,z

Detailed syntax breakdown of Axiom ax-sn

Step	Hyp	Ref	Expression
1		vz	. . . . 5 setvar z
2		vy	. . . . 5 setvar y
3	1, 2	wel 1711	. . . 4 wff z ∈ y
4		vx	. . . . 5 setvar x
5	1, 4	weq 1643	. . . 4 wff z = x
6	3, 5	wb 176	. . 3 wff (z ∈ y ↔ z = x)
7	6, 1	wal 1540	. 2 wff ∀z(z ∈ y ↔ z = x)
8	7, 2	wex 1541	1 wff ∃y∀z(z ∈ y ↔ z = x)

This axiom is referenced by:  snex  4111