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

Metamath Proof Explorer

Theorem un12

Description: A rearrangement of union. (Contributed by NM, 12-Aug-2004)

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

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