Definition df-fin5 8690

Description: A set is V-finite iff it behaves finitely under . Definition V of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)

Assertion

Ref	Expression
df-fin5

Detailed syntax breakdown of Definition df-fin5

Step	Hyp	Ref	Expression
1		cfin5 8683	. 2
2		vx	. . . . . 6
3	2	cv 1394	. . . . 5
4		c0 3784	. . . . 5
5	3, 4	wceq 1395	. . . 4
6		ccda 8568	. . . . . 6
7	3, 3, 6	co 6296	. . . . 5
8		csdm 7535	. . . . 5
9	3, 7, 8	wbr 4452	. . . 4
10	5, 9	wo 368	. . 3
11	10, 2	cab 2442	. 2
12	1, 11	wceq 1395	1

This definition is referenced by:  isfin5  8700