Metamath Proof Explorer


Theorem iunin2

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use uniiun to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004)

Ref Expression
Assertion iunin2 xABC=BxAC

Proof

Step Hyp Ref Expression
1 r19.42v xAyByCyBxAyC
2 elin yBCyByC
3 2 rexbii xAyBCxAyByC
4 eliun yxACxAyC
5 4 anbi2i yByxACyBxAyC
6 1 3 5 3bitr4i xAyBCyByxAC
7 eliun yxABCxAyBC
8 elin yBxACyByxAC
9 6 7 8 3bitr4i yxABCyBxAC
10 9 eqriv xABC=BxAC