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