Metamath Proof Explorer

Theorem inunissunidif

Description: Theorem about subsets of the difference of unions. (Contributed by ML, 29-Mar-2021)

Ref Expression
Assertion inunissunidif 
|- ( ( A i^i U. C ) = (/) -> ( A C_ U. B <-> A C_ U. ( B \ C ) ) )

Proof

Step Hyp Ref Expression
1 reldisj 
 |-  ( A C_ U. B -> ( ( A i^i U. C ) = (/) <-> A C_ ( U. B \ U. C ) ) )
2 difunieq 
 |-  ( U. B \ U. C ) C_ U. ( B \ C )
3 sstr 
 |-  ( ( A C_ ( U. B \ U. C ) /\ ( U. B \ U. C ) C_ U. ( B \ C ) ) -> A C_ U. ( B \ C ) )
4 2 3 mpan2 
 |-  ( A C_ ( U. B \ U. C ) -> A C_ U. ( B \ C ) )
5 1 4 syl6bi 
 |-  ( A C_ U. B -> ( ( A i^i U. C ) = (/) -> A C_ U. ( B \ C ) ) )
6 5 com12 
 |-  ( ( A i^i U. C ) = (/) -> ( A C_ U. B -> A C_ U. ( B \ C ) ) )
7 difss 
 |-  ( B \ C ) C_ B
8 7 unissi 
 |-  U. ( B \ C ) C_ U. B
9 sstr 
 |-  ( ( A C_ U. ( B \ C ) /\ U. ( B \ C ) C_ U. B ) -> A C_ U. B )
10 8 9 mpan2 
 |-  ( A C_ U. ( B \ C ) -> A C_ U. B )
11 6 10 impbid1 
 |-  ( ( A i^i U. C ) = (/) -> ( A C_ U. B <-> A C_ U. ( B \ C ) ) )