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\in \mathrm{On}\to R_1\left(A\right)=\left\{x|\mathrm{rank}\left(x\right)\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	rankr1a	$$⊢A\in \mathrm{On}\to \left(x\in R_1\left(A\right)\leftrightarrow \mathrm{rank}\left(x\right)\in A\right)$$
3	2	abbi2dv	$$⊢A\in \mathrm{On}\to R_1\left(A\right)=\left\{x|\mathrm{rank}\left(x\right)\in A\right\}$$