Theorem resabs1

Description: Absorption law for restriction. Exercise 17 of TakeutiZaring p. 25. (Contributed by NM, 9-Aug-1994)

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

Proof

Step	Hyp	Ref	Expression
1		resres	⊢ ( ( 𝐴 ↾ 𝐶 ) ↾ 𝐵 ) = ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) )
2		sseqin2	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐶 ∩ 𝐵 ) = 𝐵 )
3		reseq2	⊢ ( ( 𝐶 ∩ 𝐵 ) = 𝐵 → ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 ) )
4	2 3	sylbi	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 ) )
5	1 4	syl5eq	⊢ ( 𝐵 ⊆ 𝐶 → ( ( 𝐴 ↾ 𝐶 ) ↾ 𝐵 ) = ( 𝐴 ↾ 𝐵 ) )