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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexcom4 | |
|
2 | vex | |
|
3 | 2 | elima3 | |
4 | 3 | rexbii | |
5 | eliun | |
|
6 | 5 | anbi1i | |
7 | r19.41v | |
|
8 | 6 7 | bitr4i | |
9 | 8 | exbii | |
10 | 1 4 9 | 3bitr4ri | |
11 | 2 | elima3 | |
12 | eliun | |
|
13 | 10 11 12 | 3bitr4i | |
14 | 13 | eqriv | |