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

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