Description: The image of a union is the indexed union of the images. Theorem 3K(a) of Enderton p. 50. (Contributed by NM, 9-Aug-2004) (Proof shortened by Mario Carneiro, 18-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | imauni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniiun | |
|
2 | 1 | imaeq2i | |
3 | imaiun | |
|
4 | 2 3 | eqtri | |