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