Definition df-fin 4380

Description: Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-fin	⊢ Fin = ∪ Nn

Detailed syntax breakdown of Definition df-fin

Step	Hyp	Ref	Expression
1		cfin 4376	. 2 class Fin
2		cnnc 4373	. . 3 class Nn
3	2	cuni 3891	. 2 class ∪ Nn
4	1, 3	wceq 1642	1 wff Fin = ∪ Nn

This definition is referenced by:  finex  4397  elfin  4420  sfinltfin  4535  nulnnn  4556  ncssfin  6151