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