Metamath Proof Explorer

Theorem disjssun

Description: Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion disjssun 
|- ( ( A i^i B ) = (/) -> ( A C_ ( B u. C ) <-> A C_ C ) )

Proof

Step Hyp Ref Expression
1 uneq2 
 |-  ( ( A i^i B ) = (/) -> ( ( A i^i C ) u. ( A i^i B ) ) = ( ( A i^i C ) u. (/) ) )
2 indi 
 |-  ( A i^i ( B u. C ) ) = ( ( A i^i B ) u. ( A i^i C ) )
3 2 equncomi 
 |-  ( A i^i ( B u. C ) ) = ( ( A i^i C ) u. ( A i^i B ) )
4 un0 
 |-  ( ( A i^i C ) u. (/) ) = ( A i^i C )
5 4 eqcomi 
 |-  ( A i^i C ) = ( ( A i^i C ) u. (/) )
6 1 3 5 3eqtr4g 
 |-  ( ( A i^i B ) = (/) -> ( A i^i ( B u. C ) ) = ( A i^i C ) )
7 6 eqeq1d 
 |-  ( ( A i^i B ) = (/) -> ( ( A i^i ( B u. C ) ) = A <-> ( A i^i C ) = A ) )
8 df-ss 
 |-  ( A C_ ( B u. C ) <-> ( A i^i ( B u. C ) ) = A )
9 df-ss 
 |-  ( A C_ C <-> ( A i^i C ) = A )
10 7 8 9 3bitr4g 
 |-  ( ( A i^i B ) = (/) -> ( A C_ ( B u. C ) <-> A C_ C ) )