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$

Step	Hyp	Ref	Expression
1		dftr2	$⊢ Tr Hf \leftrightarrow \forall x \forall y ((x \in y \land y \in Hf) \to x \in Hf)$
2		hfelhf	$⊢ (x \in y \land y \in Hf) \to x \in Hf$
3	2	ax-gen	$⊢ \forall y ((x \in y \land y \in Hf) \to x \in Hf)$
4	1 3	mpgbir	$⊢ Tr Hf$