New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-3c		Unicode version

---

Definition df-3c 6105

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

---

Detailed syntax breakdown of Definition df-3c

Step	Hyp	Ref	Expression
1		c3c 6095	. 2 3c
2		c0 3550	. . . 4
3		cvv 2859	. . . 4
4	2	csn 3737	. . . . 5
5	3, 4	cdif 3206	. . . 4
6	2, 3, 5	ctp 3739	. . 3
7	6	cnc 6091	. 2 Nc
8	1, 7	wceq 1642	1 3c Nc

Colors of variables: wff setvar class

This definition is referenced by:  2p1e3c  6156

Copyright terms: Public domain

W3C validator