Theorem un12

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

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

Proof

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