Metamath Proof Explorer


Theorem imauni

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 AB=xBAx

Proof

Step Hyp Ref Expression
1 uniiun B=xBx
2 1 imaeq2i AB=AxBx
3 imaiun AxBx=xBAx
4 2 3 eqtri AB=xBAx