Metamath Proof Explorer


Theorem ssinss2d

Description: Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis ssinss2d.1
|- ( ph -> B C_ C )
Assertion ssinss2d
|- ( ph -> ( A i^i B ) C_ C )

Proof

Step Hyp Ref Expression
1 ssinss2d.1
 |-  ( ph -> B C_ C )
2 incom
 |-  ( A i^i B ) = ( B i^i A )
3 1 ssinss1d
 |-  ( ph -> ( B i^i A ) C_ C )
4 2 3 eqsstrid
 |-  ( ph -> ( A i^i B ) C_ C )