Theorem unundir

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

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

Proof

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