Metamath Proof Explorer

Theorem inss

Description: Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014)

Ref Expression
Assertion inss 
|- ( ( A C_ C \/ B C_ C ) -> ( A i^i B ) C_ C )

Proof

Step Hyp Ref Expression
1 ssinss1 
 |-  ( A C_ C -> ( A i^i B ) C_ C )
2 incom 
 |-  ( A i^i B ) = ( B i^i A )
3 ssinss1 
 |-  ( B C_ C -> ( B i^i A ) C_ C )
4 2 3 eqsstrid 
 |-  ( B C_ C -> ( A i^i B ) C_ C )
5 1 4 jaoi 
 |-  ( ( A C_ C \/ B C_ C ) -> ( A i^i B ) C_ C )