Theorem r1tr2

Description: Each stage of the cumulative hierarchy of sets includes its union, that is, is transitive. JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011)

	Ref	Expression
Assertion	r1tr2	$$⊢\bigcup R_1\left(A\right)\subseteq R_1\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		r1tr	$$⊢\mathrm{Tr}{R}_1\left(A\right)$$
2		df-tr	$$⊢\mathrm{Tr}{R}_1\left(A\right)\leftrightarrow \bigcup R_1\left(A\right)\subseteq R_1\left(A\right)$$
3	1 2	mpbi	$$⊢\bigcup R_1\left(A\right)\subseteq R_1\left(A\right)$$