Metamath Proof Explorer

Theorem ssinss1

Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999)

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

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( A i^i B ) C_ A
2 sstr2 
 |-  ( ( A i^i B ) C_ A -> ( A C_ C -> ( A i^i B ) C_ C ) )
3 1 2 ax-mp 
 |-  ( A C_ C -> ( A i^i B ) C_ C )