Metamath Proof Explorer

Theorem r1sscl

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

Ref Expression
Assertion r1sscl ⊢ A ∈ R1 ⁡ B ∧ C ⊆ A → C ∈ R1 ⁡ B

Proof

Step Hyp Ref Expression
1 r1pwss ⊢ A ∈ R1 ⁡ B → 𝒫 A ⊆ R1 ⁡ B
2 1 adantr ⊢ A ∈ R1 ⁡ B ∧ C ⊆ A → 𝒫 A ⊆ R1 ⁡ B
3 elpw2g ⊢ A ∈ R1 ⁡ B → C ∈ 𝒫 A ↔ C ⊆ A
4 3 biimpar ⊢ A ∈ R1 ⁡ B ∧ C ⊆ A → C ∈ 𝒫 A
5 2 4 sseldd ⊢ A ∈ R1 ⁡ B ∧ C ⊆ A → C ∈ R1 ⁡ B