Axiom ax-1c 4081

Description: State the axiom of cardinal one. This axiom guarantees the existence of the set of all singletons, which will become cardinal one later in our development. Axiom P8 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
ax-1c	⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z))

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-1c

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

This axiom is referenced by:  1cex  4142