NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-3c GIF 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 {, V, (V {})}

Detailed syntax breakdown of Definition df-3c
StepHypRef Expression
1 c3c 6095 . 2 class 3c
2 c0 3550 . . . 4 class
3 cvv 2859 . . . 4 class V
42csn 3737 . . . . 5 class {}
53, 4cdif 3206 . . . 4 class (V {})
62, 3, 5ctp 3739 . . 3 class {, V, (V {})}
76cnc 6091 . 2 class Nc {, V, (V {})}
81, 7wceq 1642 1 wff 3c = Nc {, V, (V {})}
Colors of variables: wff setvar class
This definition is referenced by:  2p1e3c  6156
  Copyright terms: Public domain W3C validator