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

Metamath Proof Explorer

Theorem unundir

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

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

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