Metamath Proof Explorer


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