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