Definition df-fin4 9109

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	|- FinIV = { x | -. E. y ( y C. x /\ y ~~ x ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-fin4

Step	Hyp	Ref	Expression
1		cfin4 9102	. 2 class FinIV
2		vy	. . . . . . . 8 setvar y
3	2	cv 1482	. . . . . . 7 class y
4		vx	. . . . . . . 8 setvar x
5	4	cv 1482	. . . . . . 7 class x
6	3, 5	wpss 3575	. . . . . 6 wff y C. x
7		cen 7952	. . . . . . 7 class ~~
8	3, 5, 7	wbr 4653	. . . . . 6 wff y ~~ x
9	6, 8	wa 384	. . . . 5 wff ( y C. x /\ y ~~ x )
10	9, 2	wex 1704	. . . 4 wff E. y ( y C. x /\ y ~~ x )
11	10	wn 3	. . 3 wff -. E. y ( y C. x /\ y ~~ x )
12	11, 4	cab 2608	. 2 class { x | -. E. y ( y C. x /\ y ~~ x ) }
13	1, 12	wceq 1483	1 wff FinIV = { x | -. E. y ( y C. x /\ y ~~ x ) }

This definition is referenced by:  isfin4  9119