Theorem ressabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Assertion	ressabs	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ssexg	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑋 ) → 𝐵 ∈ V )
2	1	ancoms	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ V )
3		ressress	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
4	2 3	syldan	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
5		sseqin2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
6	5	bilani	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
7	6	oveq2d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 ↾s 𝐵 ) )
8	4 7	eqtrd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐵 ) )