This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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