Metamath Proof Explorer

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 
|- ( ( A u. B ) u. C ) = ( ( A u. C ) u. B )

Proof

Step Hyp Ref Expression
1 unass 
 |-  ( ( A u. B ) u. C ) = ( A u. ( B u. C ) )
2 un12 
 |-  ( A u. ( B u. C ) ) = ( B u. ( A u. C ) )
3 uncom 
 |-  ( B u. ( A u. C ) ) = ( ( A u. C ) u. B )
4 1 2 3 3eqtri 
 |-  ( ( A u. B ) u. C ) = ( ( A u. C ) u. B )