Definition df-fin4 8688

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.)

Assertion

Ref	Expression
df-fin4

Distinct variable group:   ,

Detailed syntax breakdown of Definition df-fin4

Step	Hyp	Ref	Expression
1		cfin4 8681	. 2
2		vy	. . . . . . . 8
3	2	cv 1394	. . . . . . 7
4		vx	. . . . . . . 8
5	4	cv 1394	. . . . . . 7
6	3, 5	wpss 3476	. . . . . 6
7		cen 7533	. . . . . . 7
8	3, 5, 7	wbr 4452	. . . . . 6
9	6, 8	wa 369	. . . . 5
10	9, 2	wex 1612	. . . 4
11	10	wn 3	. . 3
12	11, 4	cab 2442	. 2
13	1, 12	wceq 1395	1

This definition is referenced by:  isfin4  8698