Axiom ax-1c 4082

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	|- E.xA.y(y e. x <-> E.zA.w(w e. 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 e. x
4		vw	. . . . . . . 8 setvar w
5	4, 1	wel 1711	. . . . . . 7 wff w e. y
6		vz	. . . . . . . 8 setvar z
7	4, 6	weq 1643	. . . . . . 7 wff w = z
8	5, 7	wb 176	. . . . . 6 wff (w e. y <-> w = z)
9	8, 4	wal 1540	. . . . 5 wff A.w(w e. y <-> w = z)
10	9, 6	wex 1541	. . . 4 wff E.zA.w(w e. y <-> w = z)
11	3, 10	wb 176	. . 3 wff (y e. x <-> E.zA.w(w e. y <-> w = z))
12	11, 1	wal 1540	. 2 wff A.y(y e. x <-> E.zA.w(w e. y <-> w = z))
13	12, 2	wex 1541	1 wff E.xA.y(y e. x <-> E.zA.w(w e. y <-> w = z))

This axiom is referenced by:  1cex  4143