Theorem un23

Description: A rearrangement of union. (Contributed by NM, 12-Aug-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		unass	⊢ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) = ( 𝐴 ∪ ( 𝐵 ∪ 𝐶 ) )
2		un12	⊢ ( 𝐴 ∪ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐵 ∪ ( 𝐴 ∪ 𝐶 ) )
3		uncom	⊢ ( 𝐵 ∪ ( 𝐴 ∪ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐶 ) ∪ 𝐵 )
4	1 2 3	3eqtri	⊢ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) = ( ( 𝐴 ∪ 𝐶 ) ∪ 𝐵 )