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 |` X ) C_ B <-> ( A |` X ) C_ ( B |` X ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- X C_ X
2		resssres	|- ( X C_ X -> ( ( A |` X ) C_ B <-> ( A |` X ) C_ ( B |` X ) ) )
3	1 2	ax-mp	|- ( ( A |` X ) C_ B <-> ( A |` X ) C_ ( B |` X ) )