Theorem undisj2

Description: The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004)

	Ref	Expression
Assertion	undisj2	$$⊢\left(A\cap B=\varnothing \wedge A\cap C=\varnothing \right)\leftrightarrow A\cap \left(B\cup C\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		un00	$$⊢\left(A\cap B=\varnothing \wedge A\cap C=\varnothing \right)\leftrightarrow \left(A\cap B\right)\cup \left(A\cap C\right)=\varnothing$$
2		indi	$$⊢A\cap \left(B\cup C\right)=\left(A\cap B\right)\cup \left(A\cap C\right)$$
3	2	eqeq1i	$$⊢A\cap \left(B\cup C\right)=\varnothing \leftrightarrow \left(A\cap B\right)\cup \left(A\cap C\right)=\varnothing$$
4	1 3	bitr4i	$$⊢\left(A\cap B=\varnothing \wedge A\cap C=\varnothing \right)\leftrightarrow A\cap \left(B\cup C\right)=\varnothing$$