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

Metamath Proof Explorer

Theorem un4

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

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

Step	Hyp	Ref	Expression
1		un12	$⊢ B \cup (C \cup D) = C \cup (B \cup D)$
2	1	uneq2i	$⊢ A \cup (B \cup (C \cup D)) = A \cup (C \cup (B \cup D))$
3		unass	$⊢ (A \cup B) \cup (C \cup D) = A \cup (B \cup (C \cup D))$
4		unass	$⊢ (A \cup C) \cup (B \cup D) = A \cup (C \cup (B \cup D))$
5	2 3 4	3eqtr4i	$⊢ (A \cup B) \cup (C \cup D) = (A \cup C) \cup (B \cup D)$