# Metamath Proof Explorer

## Theorem dfimafnf

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006) (Revised by Thierry Arnoux, 24-Apr-2017)

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

### Proof

Step Hyp Ref Expression
1 dfimafnf.1
` |-  F/_ x A`
2 dfimafnf.2
` |-  F/_ x F`
3 ssel
` |-  ( A C_ dom F -> ( z e. A -> z e. dom F ) )`
4 eqcom
` |-  ( ( F ` z ) = y <-> y = ( F ` z ) )`
5 funbrfvb
` |-  ( ( Fun F /\ z e. dom F ) -> ( ( F ` z ) = y <-> z F y ) )`
6 4 5 bitr3id
` |-  ( ( Fun F /\ z e. dom F ) -> ( y = ( F ` z ) <-> z F y ) )`
7 6 ex
` |-  ( Fun F -> ( z e. dom F -> ( y = ( F ` z ) <-> z F y ) ) )`
8 3 7 syl9r
` |-  ( Fun F -> ( A C_ dom F -> ( z e. A -> ( y = ( F ` z ) <-> z F y ) ) ) )`
9 8 imp31
` |-  ( ( ( Fun F /\ A C_ dom F ) /\ z e. A ) -> ( y = ( F ` z ) <-> z F y ) )`
10 9 rexbidva
` |-  ( ( Fun F /\ A C_ dom F ) -> ( E. z e. A y = ( F ` z ) <-> E. z e. A z F y ) )`
11 10 abbidv
` |-  ( ( Fun F /\ A C_ dom F ) -> { y | E. z e. A y = ( F ` z ) } = { y | E. z e. A z F y } )`
12 dfima2
` |-  ( F " A ) = { y | E. z e. A z F y }`
13 11 12 syl6reqr
` |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. z e. A y = ( F ` z ) } )`
14 nfcv
` |-  F/_ z A`
15 nfcv
` |-  F/_ x z`
16 2 15 nffv
` |-  F/_ x ( F ` z )`
17 16 nfeq2
` |-  F/ x y = ( F ` z )`
18 nfv
` |-  F/ z y = ( F ` x )`
19 fveq2
` |-  ( z = x -> ( F ` z ) = ( F ` x ) )`
20 19 eqeq2d
` |-  ( z = x -> ( y = ( F ` z ) <-> y = ( F ` x ) ) )`
21 14 1 17 18 20 cbvrexfw
` |-  ( E. z e. A y = ( F ` z ) <-> E. x e. A y = ( F ` x ) )`
22 21 abbii
` |-  { y | E. z e. A y = ( F ` z ) } = { y | E. x e. A y = ( F ` x ) }`
23 13 22 syl6eq
` |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A y = ( F ` x ) } )`