Theorem elhf2g

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

	Ref	Expression
Assertion	elhf2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ HF ↔ ( rank ‘ 𝐴 ) ∈ ω ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ HF ↔ 𝐴 ∈ HF ) )
2		fveq2	⊢ ( 𝑥 = 𝐴 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
3	2	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) ∈ ω ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
4		vex	⊢ 𝑥 ∈ V
5	4	elhf2	⊢ ( 𝑥 ∈ HF ↔ ( rank ‘ 𝑥 ) ∈ ω )
6	1 3 5	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ HF ↔ ( rank ‘ 𝐴 ) ∈ ω ) )