Definition df-fin

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 . If we accept Infinity, we can also express A e. Fin by A ~< _om (Theorem isfinite .) (Contributed by NM, 22-Aug-2008)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfn	|- Fin
1		vx	|- x
2		vy	|- y
3		com	|- _om
4	1	cv	|- x
5		cen	|- ~~
6	2	cv	|- y
7	4 6 5	wbr	|- x ~~ y
8	7 2 3	wrex	|- E. y e. _om x ~~ y
9	8 1	cab	|- { x | E. y e. _om x ~~ y }
10	0 9	wceq	|- Fin = { x | E. y e. _om x ~~ y }