Definition df-can 6325

Description: Define the class of all Cantorian sets. These are so-called because Cantor's Theorem Nc A <_c Nc ~PA 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 | ~P1 x ~~ 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 ~P1 x
5		cen 6029	. . . 4 class ~~
6	4, 3, 5	wbr 4640	. . 3 wff ~P1 x ~~ x
7	6, 2	cab 2339	. 2 class {x | ~P1 x ~~ x}
8	1, 7	wceq 1642	1 wff Can = {x | ~P1 x ~~ x}

This definition is referenced by:  elcan  6330