Theorem hftr

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

	Ref	Expression
Assertion	hftr	$$⊢\mathrm{Tr}\mathrm{Hf}$$

Proof

Step	Hyp	Ref	Expression
1		dftr2	$$⊢\mathrm{Tr}\mathrm{Hf}\leftrightarrow \forall x\forall y\left(\left(x\in y\wedge y\in \mathrm{Hf}\right)\to x\in \mathrm{Hf}\right)$$
2		hfelhf	$$⊢\left(x\in y\wedge y\in \mathrm{Hf}\right)\to x\in \mathrm{Hf}$$
3	2	ax-gen	$$⊢\forall y\left(\left(x\in y\wedge y\in \mathrm{Hf}\right)\to x\in \mathrm{Hf}\right)$$
4	1 3	mpgbir	$$⊢\mathrm{Tr}\mathrm{Hf}$$