Metamath Proof Explorer


Theorem r1tr2

Description: The union of a cumulative hierarchy of sets at ordinal A is a subset of the hierarchy at A . JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011)

Ref Expression
Assertion r1tr2 ( 𝑅1𝐴 ) ⊆ ( 𝑅1𝐴 )

Proof

Step Hyp Ref Expression
1 r1tr Tr ( 𝑅1𝐴 )
2 df-tr ( Tr ( 𝑅1𝐴 ) ↔ ( 𝑅1𝐴 ) ⊆ ( 𝑅1𝐴 ) )
3 1 2 mpbi ( 𝑅1𝐴 ) ⊆ ( 𝑅1𝐴 )