Definition df-1c 4137

Description: Define cardinal one. This is the set of all singletons, or the set of all sets of size one. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-1c	|- 1c = {x | E.y x = {y}}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-1c

Step	Hyp	Ref	Expression
1		c1c 4135	. 2 class 1c
2		vx	. . . . . 6 setvar x
3	2	cv 1641	. . . . 5 class x
4		vy	. . . . . . 7 setvar y
5	4	cv 1641	. . . . . 6 class y
6	5	csn 3738	. . . . 5 class {y}
7	3, 6	wceq 1642	. . . 4 wff x = {y}
8	7, 4	wex 1541	. . 3 wff E.y x = {y}
9	8, 2	cab 2339	. 2 class {x | E.y x = {y}}
10	1, 9	wceq 1642	1 wff 1c = {x | E.y x = {y}}

This definition is referenced by:  el1c  4140  1cex  4143