Metamath Proof Explorer


Theorem hftr

Description: The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015)

Ref Expression
Assertion hftr Tr Hf

Proof

Step Hyp Ref Expression
1 dftr2 Tr Hf x y x y y Hf x Hf
2 hfelhf x y y Hf x Hf
3 2 ax-gen y x y y Hf x Hf
4 1 3 mpgbir Tr Hf