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

Definition df-can 6324
Description: Define the class of all Cantorian sets. These are so-called because Cantor's Theorem Nc <c Nc holds for these sets. Definition from [Rosser] p. 347 and [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
Assertion
Ref Expression
df-can Can 1

Detailed syntax breakdown of Definition df-can
StepHypRef Expression
1 ccan 6323 . 2 Can
2 vx . . . . . 6
32cv 1641 . . . . 5
43cpw1 4135 . . . 4 1
5 cen 6028 . . . 4
64, 3, 5wbr 4639 . . 3 1
76, 2cab 2339 . 2 1
81, 7wceq 1642 1 Can 1
Colors of variables: wff setvar class
This definition is referenced by:  elcan  6329
  Copyright terms: Public domain W3C validator