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\subseteq Y\to \left({A\upharpoonright }_X\subseteq B\leftrightarrow {A\upharpoonright }_X\subseteq {B\upharpoonright }_Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssres	$$⊢{A\upharpoonright }_X\subseteq B\to {\left({A\upharpoonright }_X\right)\upharpoonright }_Y\subseteq {B\upharpoonright }_Y$$
2		resabs2	$$⊢X\subseteq Y\to {\left({A\upharpoonright }_X\right)\upharpoonright }_Y={A\upharpoonright }_X$$
3	2	sseq1d	$$⊢X\subseteq Y\to \left({\left({A\upharpoonright }_X\right)\upharpoonright }_Y\subseteq {B\upharpoonright }_Y\leftrightarrow {A\upharpoonright }_X\subseteq {B\upharpoonright }_Y\right)$$
4	1 3	imbitrid	$$⊢X\subseteq Y\to \left({A\upharpoonright }_X\subseteq B\to {A\upharpoonright }_X\subseteq {B\upharpoonright }_Y\right)$$
5		id	$$⊢{A\upharpoonright }_X\subseteq {B\upharpoonright }_Y\to {A\upharpoonright }_X\subseteq {B\upharpoonright }_Y$$
6		resss	$$⊢{B\upharpoonright }_Y\subseteq B$$
7	5 6	sstrdi	$$⊢{A\upharpoonright }_X\subseteq {B\upharpoonright }_Y\to {A\upharpoonright }_X\subseteq B$$
8	4 7	impbid1	$$⊢X\subseteq Y\to \left({A\upharpoonright }_X\subseteq B\leftrightarrow {A\upharpoonright }_X\subseteq {B\upharpoonright }_Y\right)$$