Metamath Proof Explorer

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 
|- ( A C_ B -> ( C |` A ) C_ ( C |` B ) )

Proof

Step Hyp Ref Expression
1 xpss1 
 |-  ( A C_ B -> ( A X. _V ) C_ ( B X. _V ) )
2 sslin 
 |-  ( ( A X. _V ) C_ ( B X. _V ) -> ( C i^i ( A X. _V ) ) C_ ( C i^i ( B X. _V ) ) )
3 1 2 syl 
 |-  ( A C_ B -> ( C i^i ( A X. _V ) ) C_ ( C i^i ( B X. _V ) ) )
4 df-res 
 |-  ( C |` A ) = ( C i^i ( A X. _V ) )
5 df-res 
 |-  ( C |` B ) = ( C i^i ( B X. _V ) )
6 3 4 5 3sstr4g 
 |-  ( A C_ B -> ( C |` A ) C_ ( C |` B ) )