Theorem resssres

Description: A restricted class is included in a class if and only if it is included in that class restricted to any class including the first restricting class. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	resssres	|- ( X C_ Y -> ( ( A |` X ) C_ B <-> ( A |` X ) C_ ( B |` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssres	|- ( ( A |` X ) C_ B -> ( ( A |` X ) |` Y ) C_ ( B |` Y ) )
2		resabs2	|- ( X C_ Y -> ( ( A |` X ) |` Y ) = ( A |` X ) )
3	2	sseq1d	|- ( X C_ Y -> ( ( ( A |` X ) |` Y ) C_ ( B |` Y ) <-> ( A |` X ) C_ ( B |` Y ) ) )
4	1 3	imbitrid	|- ( X C_ Y -> ( ( A |` X ) C_ B -> ( A |` X ) C_ ( B |` Y ) ) )
5		id	|- ( ( A |` X ) C_ ( B |` Y ) -> ( A |` X ) C_ ( B |` Y ) )
6		resss	|- ( B |` Y ) C_ B
7	5 6	sstrdi	|- ( ( A |` X ) C_ ( B |` Y ) -> ( A |` X ) C_ B )
8	4 7	impbid1	|- ( X C_ Y -> ( ( A |` X ) C_ B <-> ( A |` X ) C_ ( B |` Y ) ) )