Definition df-fin 7959

Description: Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " a e. Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 8538. If we accept Infinity, we can also express A e. Fin by A ~< om (theorem isfinite 8549.) (Contributed by NM, 22-Aug-2008.)

Assertion

Ref	Expression
df-fin	|- Fin = { x | E. y e. om x ~~ y }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-fin

Step	Hyp	Ref	Expression
1		cfn 7955	. 2 class Fin
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		vy	. . . . . 6 setvar y
5	4	cv 1482	. . . . 5 class y
6		cen 7952	. . . . 5 class ~~
7	3, 5, 6	wbr 4653	. . . 4 wff x ~~ y
8		com 7065	. . . 4 class om
9	7, 4, 8	wrex 2913	. . 3 wff E. y e. om x ~~ y
10	9, 2	cab 2608	. 2 class { x | E. y e. om x ~~ y }
11	1, 10	wceq 1483	1 wff Fin = { x | E. y e. om x ~~ y }

This definition is referenced by:  isfi  7979  dffin1-5  9210