Definition df-3c 6106

Description: Define cardinal three. This is the set of all sets with three unique elements. (Contributed by Scott Fenton, 24-Feb-2015.)

Assertion

Ref	Expression
df-3c	|- 3c = Nc {(/), _V, (_V \ {(/)})}

Detailed syntax breakdown of Definition df-3c

Step	Hyp	Ref	Expression
1		c3c 6096	. 2 class 3c
2		c0 3551	. . . 4 class (/)
3		cvv 2860	. . . 4 class _V
4	2	csn 3738	. . . . 5 class {(/)}
5	3, 4	cdif 3207	. . . 4 class (_V \ {(/)})
6	2, 3, 5	ctp 3740	. . 3 class {(/), _V, (_V \ {(/)})}
7	6	cnc 6092	. 2 class Nc {(/), _V, (_V \ {(/)})}
8	1, 7	wceq 1642	1 wff 3c = Nc {(/), _V, (_V \ {(/)})}

This definition is referenced by:  2p1e3c  6157