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	$$⊢{\mathrm{Fin}}^{\mathrm{III}}=\left\{x|𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin3	$$class{\mathrm{Fin}}^{\mathrm{III}}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3	2	cpw	$$class𝒫x$$
4		cfin4	$$class{\mathrm{Fin}}^{\mathrm{IV}}$$
5	3 4	wcel	$$wff𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}$$
6	5 1	cab	$$class\left\{x|𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}\right\}$$
7	0 6	wceq	$$wff{\mathrm{Fin}}^{\mathrm{III}}=\left\{x|𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}\right\}$$