Metamath Proof Explorer


Theorem ssin0

Description: If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 ss2in
 |-  ( ( C C_ A /\ D C_ B ) -> ( C i^i D ) C_ ( A i^i B ) )
2 1 3adant1
 |-  ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) C_ ( A i^i B ) )
3 eqimss
 |-  ( ( A i^i B ) = (/) -> ( A i^i B ) C_ (/) )
4 3 3ad2ant1
 |-  ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( A i^i B ) C_ (/) )
5 2 4 sstrd
 |-  ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) C_ (/) )
6 ss0
 |-  ( ( C i^i D ) C_ (/) -> ( C i^i D ) = (/) )
7 5 6 syl
 |-  ( ( ( A i^i B ) = (/) /\ C C_ A /\ D C_ B ) -> ( C i^i D ) = (/) )