Theorem elhf2g

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

	Ref	Expression
Assertion	elhf2g	|- ( A e. V -> ( A e. Hf <-> ( rank ` A ) e. _om ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( x = A -> ( x e. Hf <-> A e. Hf ) )
2		fveq2	|- ( x = A -> ( rank ` x ) = ( rank ` A ) )
3	2	eleq1d	|- ( x = A -> ( ( rank ` x ) e. _om <-> ( rank ` A ) e. _om ) )
4		vex	|- x e. _V
5	4	elhf2	|- ( x e. Hf <-> ( rank ` x ) e. _om )
6	1 3 5	vtoclbg	|- ( A e. V -> ( A e. Hf <-> ( rank ` A ) e. _om ) )