Definition df-fin 4381

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 4377	. 2 class Fin
2		cnnc 4374	. . 3 class Nn
3	2	cuni 3892	. 2 class ∪ Nn
4	1, 3	wceq 1642	1 wff Fin = ∪ Nn

This definition is referenced by:  finex  4398  elfin  4421  sfinltfin  4536  nulnnn  4557  ncssfin  6152