Theorem dfimafn2

Description: Alternate definition of the image of a function as an indexed union of singletons of function values. (Contributed by Raph Levien, 20-Nov-2006)

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

Proof

Step	Hyp	Ref	Expression
1		dfimafn	|- ( ( 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 ) } )