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 ) = (/) )