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 e. ( R1 ` B ) /\ C C_ A ) -> C e. ( R1 ` B ) )

Proof

Step	Hyp	Ref	Expression
1		r1pwss	|- ( A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) )
2	1	adantr	|- ( ( A e. ( R1 ` B ) /\ C C_ A ) -> ~P A C_ ( R1 ` B ) )
3		elpw2g	|- ( A e. ( R1 ` B ) -> ( C e. ~P A <-> C C_ A ) )
4	3	biimpar	|- ( ( A e. ( R1 ` B ) /\ C C_ A ) -> C e. ~P A )
5	2 4	sseldd	|- ( ( A e. ( R1 ` B ) /\ C C_ A ) -> C e. ( R1 ` B ) )