Metamath Proof Explorer


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 } )