This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ⋃ R1 ⁡ A ⊆ R1 ⁡ A

Proof

Step Hyp Ref Expression
1 r1tr ⊢ Tr ⁡ R1 ⁡ A
2 df-tr ⊢ Tr ⁡ R1 ⁡ A ↔ ⋃ R1 ⁡ A ⊆ R1 ⁡ A
3 1 2 mpbi ⊢ ⋃ R1 ⁡ A ⊆ R1 ⁡ A