Definition df-hf 9898

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 9903. They are called the hereditarily finite sets since they are the finite sets whose members are hereditarily finite, as proved in elhf3 9906. (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 9897	. 2 class HF
2		cr1 9759	. . . 4 class 𝑅1
3		com 7875	. . . 4 class ω
4	2, 3	cima 5654	. . 3 class (𝑅1 “ ω)
5	4	cuni 4867	. 2 class ∪ (𝑅1 “ ω)
6	1, 5	wceq 1570	1 wff HF = ∪ (𝑅1 “ ω)

This definition is used by:  dfhf2  9899  elhf  9900  elhfOLD  9901  hffi  9902  elhf4  9905  ackbij2  10313  tskhf  10846  r1omfi  35719  r1omhf  35720