Metamath Proof Explorer


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 ( 𝐴 ∈ On → ( 𝑅1𝐴 ) = { 𝑥 ∣ ( rank ‘ 𝑥 ) ∈ 𝐴 } )

Proof

Step Hyp Ref Expression
1 vex 𝑥 ∈ V
2 1 rankr1a ( 𝐴 ∈ On → ( 𝑥 ∈ ( 𝑅1𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
3 2 abbi2dv ( 𝐴 ∈ On → ( 𝑅1𝐴 ) = { 𝑥 ∣ ( rank ‘ 𝑥 ) ∈ 𝐴 } )