Theorem ressabs

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

	Ref	Expression
Assertion	ressabs	|- ( ( A e. X /\ B C_ A ) -> ( ( W |`s A ) |`s B ) = ( W |`s B ) )

Proof

Step	Hyp	Ref	Expression
1		ssexg	|- ( ( B C_ A /\ A e. X ) -> B e. _V )
2	1	ancoms	|- ( ( A e. X /\ B C_ A ) -> B e. _V )
3		ressress	|- ( ( A e. X /\ B e. _V ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )
4	2 3	syldan	|- ( ( A e. X /\ B C_ A ) -> ( ( W |`s A ) |`s B ) = ( W |`s ( A i^i B ) ) )
5		simpr	|- ( ( A e. X /\ B C_ A ) -> B C_ A )
6		sseqin2	|- ( B C_ A <-> ( A i^i B ) = B )
7	5 6	sylib	|- ( ( A e. X /\ B C_ A ) -> ( A i^i B ) = B )
8	7	oveq2d	|- ( ( A e. X /\ B C_ A ) -> ( W |`s ( A i^i B ) ) = ( W |`s B ) )
9	4 8	eqtrd	|- ( ( A e. X /\ B C_ A ) -> ( ( W |`s A ) |`s B ) = ( W |`s B ) )