Definition df-hf 9942

Description: Define the class of sets belonging to the finite stages of the cumulative hierarchy of sets. This is the class of sets of finite rank by elhf2 9947. They are called the hereditarily finite sets since they are the finite sets whose members are hereditarily finite, as proved in elhf3 9950. (Contributed by Scott Fenton, 9-Jul-2015.)

Assertion

Ref	Expression
df-hf	⊢ HF = ∪ (𝑅1 “ ω)

Detailed syntax breakdown of Definition df-hf

Step	Hyp	Ref	Expression
1		chf 9941	. 2 class HF
2		cr1 9803	. . . 4 class 𝑅1
3		com 7911	. . . 4 class ω
4	2, 3	cima 5661	. . 3 class (𝑅1 “ ω)
5	4	cuni 4872	. 2 class ∪ (𝑅1 “ ω)
6	1, 5	wceq 1570	1 wff HF = ∪ (𝑅1 “ ω)

This definition is used by:  dfhf2  9943  elhf  9944  elhfOLD  9945  hffi  9946  elhf4  9949  ackbij2  10359  tskhf  10892  fineqvhfbregs  35947