Theorem r1val2

Description: The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of Monk1 p. 113. (Contributed by NM, 30-Nov-2003)

	Ref	Expression
Assertion	r1val2	|- ( A e. On -> ( R1 ` A ) = { x | ( rank ` x ) e. A } )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	rankr1a	|- ( A e. On -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
3	2	abbi2dv	|- ( A e. On -> ( R1 ` A ) = { x | ( rank ` x ) e. A } )