This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ A [⋃ B] = ⋃_{x \in B} A [x]$

Proof

Step	Hyp	Ref	Expression
1		uniiun	$⊢ ⋃ B = ⋃_{x \in B} x$
2	1	imaeq2i	$⊢ A [⋃ B] = A [⋃_{x \in B} x]$
3		imaiun	$⊢ A [⋃_{x \in B} x] = ⋃_{x \in B} A [x]$
4	2 3	eqtri	$⊢ A [⋃ B] = ⋃_{x \in B} A [x]$