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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin4	|- Fin4
1		vx	|- x
2		vy	|- y
3	2	cv	|- y
4	1	cv	|- x
5	3 4	wpss	|- y C. x
6		cen	|- ~~
7	3 4 6	wbr	|- y ~~ x
8	5 7	wa	|- ( y C. x /\ y ~~ x )
9	8 2	wex	|- E. y ( y C. x /\ y ~~ x )
10	9	wn	|- -. E. y ( y C. x /\ y ~~ x )
11	10 1	cab	|- { x | -. E. y ( y C. x /\ y ~~ x ) }
12	0 11	wceq	|- Fin4 = { x | -. E. y ( y C. x /\ y ~~ x ) }