Metamath Proof Explorer

Theorem unass

Description: Associative law for union of classes. Exercise 8 of TakeutiZaring p. 17. (Contributed by NM, 3-May-1994) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		elun	$⊢ x \in (A \cup (B \cup C)) \leftrightarrow (x \in A \lor x \in (B \cup C))$
2		elun	$⊢ x \in (B \cup C) \leftrightarrow (x \in B \lor x \in C)$
3	2	orbi2i	$⊢ (x \in A \lor x \in (B \cup C)) \leftrightarrow (x \in A \lor (x \in B \lor x \in C))$
4		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
5	4	orbi1i	$⊢ (x \in (A \cup B) \lor x \in C) \leftrightarrow ((x \in A \lor x \in B) \lor x \in C)$
6		orass	$⊢ ((x \in A \lor x \in B) \lor x \in C) \leftrightarrow (x \in A \lor (x \in B \lor x \in C))$
7	5 6	bitr2i	$⊢ (x \in A \lor (x \in B \lor x \in C)) \leftrightarrow (x \in (A \cup B) \lor x \in C)$
8	1 3 7	3bitrri	$⊢ (x \in (A \cup B) \lor x \in C) \leftrightarrow x \in (A \cup (B \cup C))$
9	8	uneqri	$⊢ (A \cup B) \cup C = A \cup (B \cup C)$