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 ( 𝐴 𝐵 ) = 𝑥𝐵 ( 𝐴𝑥 )