Definition df-fin4

Description: A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of Levy58 p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Assertion	df-fin4	$$⊢{\mathrm{Fin}}^{\mathrm{IV}}=\left\{x|\neg \exists y\left(y\subset x\wedge y\approx x\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin4	$$class{\mathrm{Fin}}^{\mathrm{IV}}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	2	cv	$$setvary$$
4	1	cv	$$setvarx$$
5	3 4	wpss	$$wffy\subset x$$
6		cen	$$class\approx$$
7	3 4 6	wbr	$$wffy\approx x$$
8	5 7	wa	$$wff\left(y\subset x\wedge y\approx x\right)$$
9	8 2	wex	$$wff\exists y\left(y\subset x\wedge y\approx x\right)$$
10	9	wn	$$wff\neg \exists y\left(y\subset x\wedge y\approx x\right)$$
11	10 1	cab	$$class\left\{x|\neg \exists y\left(y\subset x\wedge y\approx x\right)\right\}$$
12	0 11	wceq	$$wff{\mathrm{Fin}}^{\mathrm{IV}}=\left\{x|\neg \exists y\left(y\subset x\wedge y\approx x\right)\right\}$$