Definition df-2c 6104

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

Assertion

Ref	Expression
df-2c	⊢ 2c = Nc {∅, V}

Detailed syntax breakdown of Definition df-2c

Step	Hyp	Ref	Expression
1		c2c 6094	. 2 class 2c
2		c0 3550	. . . 4 class ∅
3		cvv 2859	. . . 4 class V
4	2, 3	cpr 3738	. . 3 class {∅, V}
5	4	cnc 6091	. 2 class Nc {∅, V}
6	1, 5	wceq 1642	1 wff 2c = Nc {∅, V}

This definition is referenced by:  1p1e2c  6155  2p1e3c  6156  nncdiv3lem2  6274