NFE Home 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
StepHypRef Expression
1 c3c 6095 . 2 3c
2 c0 3550 . . . 4
3 cvv 2859 . . . 4
42csn 3737 . . . . 5
53, 4cdif 3206 . . . 4
62, 3, 5ctp 3739 . . 3
76cnc 6091 . 2 Nc
81, 7wceq 1642 1 3c Nc
Colors of variables: wff setvar class
This definition is referenced by:  2p1e3c  6156
  Copyright terms: Public domain W3C validator