Theorem unundi

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

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

Proof

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