r1sscl

Description: Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	r1sscl	$⊢ (A \in R_{1} (B) \land C \subseteq A) \to C \in R_{1} (B)$

Step	Hyp	Ref	Expression
1		r1pwss	$⊢ A \in R_{1} (B) \to 𝒫 A \subseteq R_{1} (B)$
2	1	adantr	$⊢ (A \in R_{1} (B) \land C \subseteq A) \to 𝒫 A \subseteq R_{1} (B)$
3		elpw2g	$⊢ A \in R_{1} (B) \to (C \in 𝒫 A \leftrightarrow C \subseteq A)$
4	3	biimpar	$⊢ (A \in R_{1} (B) \land C \subseteq A) \to C \in 𝒫 A$
5	2 4	sseldd	$⊢ (A \in R_{1} (B) \land C \subseteq A) \to C \in R_{1} (B)$

Metamath Proof Explorer