Definition df-fin 8737

Description: Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 ∈ Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 9399. If we accept Infinity, we can also express 𝐴 ∈ Fin by 𝐴 ≺ ω (Theorem isfinite 9410.) (Contributed by NM, 22-Aug-2008.)

Assertion

Ref	Expression
df-fin	⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-fin

Step	Hyp	Ref	Expression
1		cfn 8733	. 2 class Fin
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1538	. . . . 5 class 𝑥
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1538	. . . . 5 class 𝑦
6		cen 8730	. . . . 5 class ≈
7	3, 5, 6	wbr 5074	. . . 4 wff 𝑥 ≈ 𝑦
8		com 7712	. . . 4 class ω
9	7, 4, 8	wrex 3065	. . 3 wff ∃𝑦 ∈ ω 𝑥 ≈ 𝑦
10	9, 2	cab 2715	. 2 class {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}
11	1, 10	wceq 1539	1 wff Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}

This definition is referenced by:  isfi  8764  dffin1-5  10144