Definition df-fin3

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)

	Ref	Expression
Assertion	df-fin3	|- Fin3 = { x | ~P x e. Fin4 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin3	|- Fin3
1		vx	|- x
2	1	cv	|- x
3	2	cpw	|- ~P x
4		cfin4	|- Fin4
5	3 4	wcel	|- ~P x e. Fin4
6	5 1	cab	|- { x | ~P x e. Fin4 }
7	0 6	wceq	|- Fin3 = { x | ~P x e. Fin4 }