Theorem dfaimafn2

Description: Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	dfaimafn2	|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = U_ x e. A { ( F ''' x ) } )

Proof

Step	Hyp	Ref	Expression
1		dfaimafn	|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A ( F ''' x ) = y } )
2		iunab	|- U_ x e. A { y | ( F ''' x ) = y } = { y | E. x e. A ( F ''' x ) = y }
3	1 2	eqtr4di	|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = U_ x e. A { y | ( F ''' x ) = y } )
4		df-sn	|- { ( F ''' x ) } = { y | y = ( F ''' x ) }
5		eqcom	|- ( y = ( F ''' x ) <-> ( F ''' x ) = y )
6	5	abbii	|- { y | y = ( F ''' x ) } = { y | ( F ''' x ) = y }
7	4 6	eqtri	|- { ( F ''' x ) } = { y | ( F ''' x ) = y }
8	7	a1i	|- ( x e. A -> { ( F ''' x ) } = { y | ( F ''' x ) = y } )
9	8	iuneq2i	|- U_ x e. A { ( F ''' x ) } = U_ x e. A { y | ( F ''' x ) = y }
10	3 9	eqtr4di	|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = U_ x e. A { ( F ''' x ) } )