Definition df-can 6325

Description: Define the class of all Cantorian sets. These are so-called because Cantor's Theorem Nc A <_c Nc ℘A 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 = {x ∣ ℘1x ≈ x}

Detailed syntax breakdown of Definition df-can

Step	Hyp	Ref	Expression
1		ccan 6324	. 2 class Can
2		vx	. . . . . 6 setvar x
3	2	cv 1641	. . . . 5 class x
4	3	cpw1 4136	. . . 4 class ℘1x
5		cen 6029	. . . 4 class ≈
6	4, 3, 5	wbr 4640	. . 3 wff ℘1x ≈ x
7	6, 2	cab 2339	. 2 class {x ∣ ℘1x ≈ x}
8	1, 7	wceq 1642	1 wff Can = {x ∣ ℘1x ≈ x}

This definition is referenced by:  elcan  6330