Definition df-fin3 9110

Description: A set is III-finite (weakly Dedekind finite) iff its power set is Dedekind finite. Definition III of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)

Assertion

Ref	Expression
df-fin3	|- FinIII = { x | ~P x e. FinIV }

Detailed syntax breakdown of Definition df-fin3

Step	Hyp	Ref	Expression
1		cfin3 9103	. 2 class FinIII
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4	3	cpw 4158	. . . 4 class ~P x
5		cfin4 9102	. . . 4 class FinIV
6	4, 5	wcel 1990	. . 3 wff ~P x e. FinIV
7	6, 2	cab 2608	. 2 class { x | ~P x e. FinIV }
8	1, 7	wceq 1483	1 wff FinIII = { x | ~P x e. FinIV }

This definition is referenced by:  isfin3  9118