Theorem r1sscl

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

	Ref	Expression
Assertion	r1sscl	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		r1pwss	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) )
3		elpw2g	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝐶 ∈ 𝒫 𝐴 ↔ 𝐶 ⊆ 𝐴 ) )
4	3	biimpar	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ∈ 𝒫 𝐴 )
5	2 4	sseldd	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ∈ ( 𝑅1 ‘ 𝐵 ) )