Theorem ssres2

Description: Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	ssres2	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↾ 𝐴 ) ⊆ ( 𝐶 ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xpss1	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 × V ) ⊆ ( 𝐵 × V ) )
2		sslin	⊢ ( ( 𝐴 × V ) ⊆ ( 𝐵 × V ) → ( 𝐶 ∩ ( 𝐴 × V ) ) ⊆ ( 𝐶 ∩ ( 𝐵 × V ) ) )
3	1 2	syl	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∩ ( 𝐴 × V ) ) ⊆ ( 𝐶 ∩ ( 𝐵 × V ) ) )
4		df-res	⊢ ( 𝐶 ↾ 𝐴 ) = ( 𝐶 ∩ ( 𝐴 × V ) )
5		df-res	⊢ ( 𝐶 ↾ 𝐵 ) = ( 𝐶 ∩ ( 𝐵 × V ) )
6	3 4 5	3sstr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↾ 𝐴 ) ⊆ ( 𝐶 ↾ 𝐵 ) )