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	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		uneq2	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ∅ ) )
2		indi	⊢ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∩ 𝐶 ) )
3	2	equncomi	⊢ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐴 ∩ 𝐵 ) )
4		un0	⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ ∅ ) = ( 𝐴 ∩ 𝐶 )
5	4	eqcomi	⊢ ( 𝐴 ∩ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ∅ )
6	1 3 5	3eqtr4g	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐴 ∩ 𝐶 ) )
7	6	eqeq1d	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 𝐴 ) )
8		dfss2	⊢ ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝐴 )
9		dfss2	⊢ ( 𝐴 ⊆ 𝐶 ↔ ( 𝐴 ∩ 𝐶 ) = 𝐴 )
10	7 8 9	3bitr4g	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐶 ) )