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 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Hf ) → 𝑥 ∈ Hf ) )
2		hfelhf	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Hf ) → 𝑥 ∈ Hf )
3	2	ax-gen	⊢ ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Hf ) → 𝑥 ∈ Hf )
4	1 3	mpgbir	⊢ Tr Hf