Definition df-hf 32280

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 = U. ( R1 " om )

Detailed syntax breakdown of Definition df-hf

Step	Hyp	Ref	Expression
1		chf 32279	. 2 class Hf
2		cr1 8625	. . . 4 class R1
3		com 7065	. . . 4 class om
4	2, 3	cima 5117	. . 3 class ( R1 " om )
5	4	cuni 4436	. 2 class U. ( R1 " om )
6	1, 5	wceq 1483	1 wff Hf = U. ( R1 " om )

This definition is referenced by:  elhf  32281