Metamath Proof Explorer


Theorem un12

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

Ref Expression
Assertion un12 A B C = B A C

Proof

Step Hyp Ref Expression
1 uncom A B = B A
2 1 uneq1i A B C = B A C
3 unass A B C = A B C
4 unass B A C = B A C
5 2 3 4 3eqtr3i A B C = B A C