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 ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } )

Proof

Step Hyp Ref Expression
1 dffn5 ( 𝐹 Fn 𝐴𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
2 rneq ( 𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) → ran 𝐹 = ran ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
3 1 2 sylbi ( 𝐹 Fn 𝐴 → ran 𝐹 = ran ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
4 eqid ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) )
5 4 rnmpt ran ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) }
6 3 5 syl6eq ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } )