Metamath Proof Explorer


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 = R1 ω

Detailed syntax breakdown

Step Hyp Ref Expression
0 chf class Hf
1 cr1 class R1
2 com class ω
3 1 2 cima class R1 ω
4 3 cuni class R1 ω
5 0 4 wceq wff Hf = R1 ω