Theorem resssres0

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

	Ref	Expression
Assertion	resssres0	$$⊢{A\upharpoonright }_X\subseteq B\leftrightarrow {A\upharpoonright }_X\subseteq {B\upharpoonright }_X$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢X\subseteq X$$
2		resssres	$$⊢X\subseteq X\to \left({A\upharpoonright }_X\subseteq B\leftrightarrow {A\upharpoonright }_X\subseteq {B\upharpoonright }_X\right)$$
3	1 2	ax-mp	$$⊢{A\upharpoonright }_X\subseteq B\leftrightarrow {A\upharpoonright }_X\subseteq {B\upharpoonright }_X$$