Theorem fnima

Description: The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	fnima	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
2		fnresdm	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
3	2	rneqd	⊢ ( 𝐹 Fn 𝐴 → ran ( 𝐹 ↾ 𝐴 ) = ran 𝐹 )
4	1 3	eqtrid	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )