# 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}\cap {B}=\varnothing \to \left({A}\subseteq {B}\cup {C}↔{A}\subseteq {C}\right)$

### Proof

Step Hyp Ref Expression
1 uneq2 ${⊢}{A}\cap {B}=\varnothing \to \left({A}\cap {C}\right)\cup \left({A}\cap {B}\right)=\left({A}\cap {C}\right)\cup \varnothing$
2 indi ${⊢}{A}\cap \left({B}\cup {C}\right)=\left({A}\cap {B}\right)\cup \left({A}\cap {C}\right)$
3 2 equncomi ${⊢}{A}\cap \left({B}\cup {C}\right)=\left({A}\cap {C}\right)\cup \left({A}\cap {B}\right)$
4 un0 ${⊢}\left({A}\cap {C}\right)\cup \varnothing ={A}\cap {C}$
5 4 eqcomi ${⊢}{A}\cap {C}=\left({A}\cap {C}\right)\cup \varnothing$
6 1 3 5 3eqtr4g ${⊢}{A}\cap {B}=\varnothing \to {A}\cap \left({B}\cup {C}\right)={A}\cap {C}$
7 6 eqeq1d ${⊢}{A}\cap {B}=\varnothing \to \left({A}\cap \left({B}\cup {C}\right)={A}↔{A}\cap {C}={A}\right)$
8 df-ss ${⊢}{A}\subseteq {B}\cup {C}↔{A}\cap \left({B}\cup {C}\right)={A}$
9 df-ss ${⊢}{A}\subseteq {C}↔{A}\cap {C}={A}$
10 7 8 9 3bitr4g ${⊢}{A}\cap {B}=\varnothing \to \left({A}\subseteq {B}\cup {C}↔{A}\subseteq {C}\right)$