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

Metamath Proof Explorer

Theorem un23

Description: A rearrangement of union. (Contributed by NM, 12-Aug-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Step	Hyp	Ref	Expression
1		unass	$⊢ (A \cup B) \cup C = A \cup (B \cup C)$
2		un12	$⊢ A \cup (B \cup C) = B \cup (A \cup C)$
3		uncom	$⊢ B \cup (A \cup C) = (A \cup C) \cup B$
4	1 2 3	3eqtri	$⊢ (A \cup B) \cup C = (A \cup C) \cup B$