This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )