Definition df-hf 9910

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 9915. They are called the hereditarily finite sets since they are the finite sets whose members are hereditarily finite, as proved in elhf3 9918. (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 9909	. 2 class HF
2		cr1 9771	. . . 4 class 𝑅1
3		com 7879	. . . 4 class ω
4	2, 3	cima 5653	. . 3 class (𝑅1 “ ω)
5	4	cuni 4866	. 2 class ∪ (𝑅1 “ ω)
6	1, 5	wceq 1569	1 wff HF = ∪ (𝑅1 “ ω)

This definition is used by:  dfhf2  9911  elhf  9912  elhfOLD  9913  hffi  9914  elhf4  9917  ackbij2  10325  tskhf  10858  r1omfi  35784  r1omhf  35785