Metamath Proof Explorer


Theorem unundir

Description: Union distributes over itself. (Contributed by NM, 17-Aug-2004)

Ref Expression
Assertion unundir ABC=ACBC

Proof

Step Hyp Ref Expression
1 unidm CC=C
2 1 uneq2i ABCC=ABC
3 un4 ABCC=ACBC
4 2 3 eqtr3i ABC=ACBC