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	⊢ ( 𝐴 “ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 “ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		uniiun	⊢ ∪ 𝐵 = ∪ 𝑥 ∈ 𝐵 𝑥
2	1	imaeq2i	⊢ ( 𝐴 “ ∪ 𝐵 ) = ( 𝐴 “ ∪ 𝑥 ∈ 𝐵 𝑥 )
3		imaiun	⊢ ( 𝐴 “ ∪ 𝑥 ∈ 𝐵 𝑥 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 “ 𝑥 )
4	2 3	eqtri	⊢ ( 𝐴 “ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 “ 𝑥 )