Definition df-hf 36174

Description: Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (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 36173	. 2 class Hf
2		cr1 9802	. . . 4 class 𝑅1
3		com 7887	. . . 4 class ω
4	2, 3	cima 5688	. . 3 class (𝑅1 “ ω)
5	4	cuni 4907	. 2 class ∪ (𝑅1 “ ω)
6	1, 5	wceq 1540	1 wff Hf = ∪ (𝑅1 “ ω)

This definition is referenced by:  elhf  36175