Metamath Proof Explorer

Theorem ssdisj

Description: Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007) (Proof shortened by JJ, 14-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 ssrin 
 |-  ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )
2 eqimss 
 |-  ( ( B i^i C ) = (/) -> ( B i^i C ) C_ (/) )
3 1 2 sylan9ss 
 |-  ( ( A C_ B /\ ( B i^i C ) = (/) ) -> ( A i^i C ) C_ (/) )
4 ss0 
 |-  ( ( A i^i C ) C_ (/) -> ( A i^i C ) = (/) )
5 3 4 syl 
 |-  ( ( A C_ B /\ ( B i^i C ) = (/) ) -> ( A i^i C ) = (/) )