This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem undisj2

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

		Ref	Expression
	Assertion	undisj2	$⊢ (A \cap B = \emptyset \land A \cap C = \emptyset) \leftrightarrow A \cap (B \cup C) = \emptyset$

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