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