Metamath Proof Explorer

Theorem ssrin

Description: Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion ssrin 
|- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
2 1 anim1d 
 |-  ( A C_ B -> ( ( x e. A /\ x e. C ) -> ( x e. B /\ x e. C ) ) )
3 elin 
 |-  ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4 elin 
 |-  ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5 2 3 4 3imtr4g 
 |-  ( A C_ B -> ( x e. ( A i^i C ) -> x e. ( B i^i C ) ) )
6 5 ssrdv 
 |-  ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )