Definition df-hf

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chf	⊢ Hf
1		cr1	⊢ 𝑅1
2		com	⊢ ω
3	1 2	cima	⊢ ( 𝑅1 “ ω )
4	3	cuni	⊢ ∪ ( 𝑅1 “ ω )
5	0 4	wceq	⊢ Hf = ∪ ( 𝑅1 “ ω )