Theorem fvimage

Description: Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	fvimage	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅 “ 𝐴 ) ∈ 𝑊 ) → ( Image 𝑅 ‘ 𝐴 ) = ( 𝑅 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		imaeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝐴 ) )
3		imageval	⊢ Image 𝑅 = ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) )
4	2 3	fvmptg	⊢ ( ( 𝐴 ∈ V ∧ ( 𝑅 “ 𝐴 ) ∈ 𝑊 ) → ( Image 𝑅 ‘ 𝐴 ) = ( 𝑅 “ 𝐴 ) )
5	1 4	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅 “ 𝐴 ) ∈ 𝑊 ) → ( Image 𝑅 ‘ 𝐴 ) = ( 𝑅 “ 𝐴 ) )