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 <-> A. x A. y ( ( x e. y /\ y e. Hf ) -> x e. Hf ) )
2 hfelhf 
 |-  ( ( x e. y /\ y e. Hf ) -> x e. Hf )
3 2 ax-gen 
 |-  A. y ( ( x e. y /\ y e. Hf ) -> x e. Hf )
4 1 3 mpgbir 
 |-  Tr Hf