Theorem elhf2g

Description: Hereditarily finiteness via rank. Closed form of elhf2 . (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	elhf2g	$$⊢A\in V\to \left(A\in \mathrm{Hf}\leftrightarrow \mathrm{rank}\left(A\right)\in \mathrm{\omega }\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢x=A\to \left(x\in \mathrm{Hf}\leftrightarrow A\in \mathrm{Hf}\right)$$
2		fveq2	$$⊢x=A\to \mathrm{rank}\left(x\right)=\mathrm{rank}\left(A\right)$$
3	2	eleq1d	$$⊢x=A\to \left(\mathrm{rank}\left(x\right)\in \mathrm{\omega }\leftrightarrow \mathrm{rank}\left(A\right)\in \mathrm{\omega }\right)$$
4		vex	$$⊢x\in \mathrm{V}$$
5	4	elhf2	$$⊢x\in \mathrm{Hf}\leftrightarrow \mathrm{rank}\left(x\right)\in \mathrm{\omega }$$
6	1 3 5	vtoclbg	$$⊢A\in V\to \left(A\in \mathrm{Hf}\leftrightarrow \mathrm{rank}\left(A\right)\in \mathrm{\omega }\right)$$