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	⊢ ( ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 ↔ ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ 𝑋 ⊆ 𝑋
2		resssres	⊢ ( 𝑋 ⊆ 𝑋 → ( ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 ↔ ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑋 ) ) )
3	1 2	ax-mp	⊢ ( ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 ↔ ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑋 ) )