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\leftrightarrow 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\leftrightarrow A\cap C=A\right)$$
8		df-ss	$$⊢A\subseteq B\cup C\leftrightarrow A\cap \left(B\cup C\right)=A$$
9		df-ss	$$⊢A\subseteq C\leftrightarrow A\cap C=A$$
10	7 8 9	3bitr4g	$$⊢A\cap B=\varnothing \to \left(A\subseteq B\cup C\leftrightarrow A\subseteq C\right)$$