Theorem fnrnfv

Description: The range of a function expressed as a collection of the function's values. (Contributed by NM, 20-Oct-2005) (Proof shortened by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	fnrnfv	|- ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )

Proof

Step	Hyp	Ref	Expression
1		dffn5	|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
2		rneq	|- ( F = ( x e. A |-> ( F ` x ) ) -> ran F = ran ( x e. A |-> ( F ` x ) ) )
3	1 2	sylbi	|- ( F Fn A -> ran F = ran ( x e. A |-> ( F ` x ) ) )
4		eqid	|- ( x e. A |-> ( F ` x ) ) = ( x e. A |-> ( F ` x ) )
5	4	rnmpt	|- ran ( x e. A |-> ( F ` x ) ) = { y | E. x e. A y = ( F ` x ) }
6	3 5	eqtrdi	|- ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )