Metamath Proof Explorer


Theorem r1sssuc

Description: The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011)

Ref Expression
Assertion r1sssuc A On R1 A R1 suc A

Proof

Step Hyp Ref Expression
1 r1tr Tr R1 A
2 dftr4 Tr R1 A R1 A 𝒫 R1 A
3 1 2 mpbi R1 A 𝒫 R1 A
4 r1suc A On R1 suc A = 𝒫 R1 A
5 3 4 sseqtrrid A On R1 A R1 suc A