Theorem inunissunidif

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

	Ref	Expression
Assertion	inunissunidif	⊢ ( ( 𝐴 ∩ ∪ 𝐶 ) = ∅ → ( 𝐴 ⊆ ∪ 𝐵 ↔ 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		reldisj	⊢ ( 𝐴 ⊆ ∪ 𝐵 → ( ( 𝐴 ∩ ∪ 𝐶 ) = ∅ ↔ 𝐴 ⊆ ( ∪ 𝐵 ∖ ∪ 𝐶 ) ) )
2		difunieq	⊢ ( ∪ 𝐵 ∖ ∪ 𝐶 ) ⊆ ∪ ( 𝐵 ∖ 𝐶 )
3		sstr	⊢ ( ( 𝐴 ⊆ ( ∪ 𝐵 ∖ ∪ 𝐶 ) ∧ ( ∪ 𝐵 ∖ ∪ 𝐶 ) ⊆ ∪ ( 𝐵 ∖ 𝐶 ) ) → 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) )
4	2 3	mpan2	⊢ ( 𝐴 ⊆ ( ∪ 𝐵 ∖ ∪ 𝐶 ) → 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) )
5	1 4	biimtrdi	⊢ ( 𝐴 ⊆ ∪ 𝐵 → ( ( 𝐴 ∩ ∪ 𝐶 ) = ∅ → 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) ) )
6	5	com12	⊢ ( ( 𝐴 ∩ ∪ 𝐶 ) = ∅ → ( 𝐴 ⊆ ∪ 𝐵 → 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) ) )
7		difss	⊢ ( 𝐵 ∖ 𝐶 ) ⊆ 𝐵
8	7	unissi	⊢ ∪ ( 𝐵 ∖ 𝐶 ) ⊆ ∪ 𝐵
9		sstr	⊢ ( ( 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) ∧ ∪ ( 𝐵 ∖ 𝐶 ) ⊆ ∪ 𝐵 ) → 𝐴 ⊆ ∪ 𝐵 )
10	8 9	mpan2	⊢ ( 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) → 𝐴 ⊆ ∪ 𝐵 )
11	6 10	impbid1	⊢ ( ( 𝐴 ∩ ∪ 𝐶 ) = ∅ → ( 𝐴 ⊆ ∪ 𝐵 ↔ 𝐴 ⊆ ∪ ( 𝐵 ∖ 𝐶 ) ) )