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	|- ( A " U. B ) = U_ x e. B ( A " x )

Proof

Step	Hyp	Ref	Expression
1		uniiun	|- U. B = U_ x e. B x
2	1	imaeq2i	|- ( A " U. B ) = ( A " U_ x e. B x )
3		imaiun	|- ( A " U_ x e. B x ) = U_ x e. B ( A " x )
4	2 3	eqtri	|- ( A " U. B ) = U_ x e. B ( A " x )