Metamath Proof Explorer


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 𝑅𝐴 ) = ( 𝑅𝐴 ) )