![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > df-fin | GIF version |
Description: Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.) |
Ref | Expression |
---|---|
df-fin | ⊢ Fin = ∪ Nn |
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 |
Colors of variables: wff setvar class |
This definition is referenced by: finex 4397 elfin 4420 sfinltfin 4535 nulnnn 4556 ncssfin 6151 |
Copyright terms: Public domain | W3C validator |