Metamath Proof Explorer


Theorem 2iunin

Description: Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008)

Ref Expression
Assertion 2iunin xAyBCD=xACyBD

Proof

Step Hyp Ref Expression
1 iunin2 yBCD=CyBD
2 1 a1i xAyBCD=CyBD
3 2 iuneq2i xAyBCD=xACyBD
4 iunin1 xACyBD=xACyBD
5 3 4 eqtri xAyBCD=xACyBD