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