Definition df-2c 6105

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 6095	. 2 class 2c
2		c0 3551	. . . 4 class (/)
3		cvv 2860	. . . 4 class _V
4	2, 3	cpr 3739	. . 3 class {(/), _V}
5	4	cnc 6092	. 2 class Nc {(/), _V}
6	1, 5	wceq 1642	1 wff 2c = Nc {(/), _V}

This definition is referenced by:  1p1e2c  6156  2p1e3c  6157  nncdiv3lem2  6277