Metamath Proof Explorer


Theorem imaiun

Description: The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion imaiun AxBC=xBAC

Proof

Step Hyp Ref Expression
1 rexcom4 xBzzCzyAzxBzCzyA
2 vex yV
3 2 elima3 yACzzCzyA
4 3 rexbii xByACxBzzCzyA
5 eliun zxBCxBzC
6 5 anbi1i zxBCzyAxBzCzyA
7 r19.41v xBzCzyAxBzCzyA
8 6 7 bitr4i zxBCzyAxBzCzyA
9 8 exbii zzxBCzyAzxBzCzyA
10 1 4 9 3bitr4ri zzxBCzyAxByAC
11 2 elima3 yAxBCzzxBCzyA
12 eliun yxBACxByAC
13 10 11 12 3bitr4i yAxBCyxBAC
14 13 eqriv AxBC=xBAC