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

Metamath Proof Explorer

Theorem unundi

Description: Union distributes over itself. (Contributed by NM, 17-Aug-2004)

		Ref	Expression
	Assertion	unundi	$⊢ A \cup (B \cup C) = (A \cup B) \cup (A \cup C)$

Step	Hyp	Ref	Expression
1		unidm	$⊢ A \cup A = A$
2	1	uneq1i	$⊢ (A \cup A) \cup (B \cup C) = A \cup (B \cup C)$
3		un4	$⊢ (A \cup A) \cup (B \cup C) = (A \cup B) \cup (A \cup C)$
4	2 3	eqtr3i	$⊢ A \cup (B \cup C) = (A \cup B) \cup (A \cup C)$