Theorem un12

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

	Ref	Expression
Assertion	un12	⊢ ( 𝐴 ∪ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐵 ∪ ( 𝐴 ∪ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐴 )
2	1	uneq1i	⊢ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) = ( ( 𝐵 ∪ 𝐴 ) ∪ 𝐶 )
3		unass	⊢ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) = ( 𝐴 ∪ ( 𝐵 ∪ 𝐶 ) )
4		unass	⊢ ( ( 𝐵 ∪ 𝐴 ) ∪ 𝐶 ) = ( 𝐵 ∪ ( 𝐴 ∪ 𝐶 ) )
5	2 3 4	3eqtr3i	⊢ ( 𝐴 ∪ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐵 ∪ ( 𝐴 ∪ 𝐶 ) )