Theorem dfimafn

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006)

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

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( A C_ dom F -> ( x e. A -> x e. dom F ) )
2		funbrfvb	|- ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = y <-> x F y ) )
3	2	ex	|- ( Fun F -> ( x e. dom F -> ( ( F ` x ) = y <-> x F y ) ) )
4	1 3	syl9r	|- ( Fun F -> ( A C_ dom F -> ( x e. A -> ( ( F ` x ) = y <-> x F y ) ) ) )
5	4	imp31	|- ( ( ( Fun F /\ A C_ dom F ) /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
6	5	rexbidva	|- ( ( Fun F /\ A C_ dom F ) -> ( E. x e. A ( F ` x ) = y <-> E. x e. A x F y ) )
7	6	abbidv	|- ( ( Fun F /\ A C_ dom F ) -> { y | E. x e. A ( F ` x ) = y } = { y | E. x e. A x F y } )
8		dfima2	|- ( F " A ) = { y | E. x e. A x F y }
9	7 8	syl6reqr	|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A ( F ` x ) = y } )