Theorem fnrnafv

Description: The range of a function expressed as a collection of the function's values, analogous to fnrnfv . (Contributed by Alexander van der Vekens, 25-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dfafn5a	|- ( F Fn A -> F = ( x e. A |-> ( F ''' x ) ) )
2	1	rneqd	|- ( F Fn A -> ran F = ran ( x e. A |-> ( F ''' x ) ) )
3		eqid	|- ( x e. A |-> ( F ''' x ) ) = ( x e. A |-> ( F ''' x ) )
4	3	rnmpt	|- ran ( x e. A |-> ( F ''' x ) ) = { y | E. x e. A y = ( F ''' x ) }
5	2 4	eqtrdi	|- ( F Fn A -> ran F = { y | E. x e. A y = ( F ''' x ) } )