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 FFnAranF=y|xAy=Fx

Proof

Step Hyp Ref Expression
1 dffn5 FFnAF=xAFx
2 rneq F=xAFxranF=ranxAFx
3 1 2 sylbi FFnAranF=ranxAFx
4 eqid xAFx=xAFx
5 4 rnmpt ranxAFx=y|xAy=Fx
6 3 5 eqtrdi FFnAranF=y|xAy=Fx