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 𝑅 ‘ 𝐴 ) = ( 𝑅 “ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) | |
2 | imaeq2 | ⊢ ( 𝑥 = 𝐴 → ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝐴 ) ) | |
3 | imageval | ⊢ Image 𝑅 = ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) | |
4 | 2 3 | fvmptg | ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑅 “ 𝐴 ) ∈ 𝑊 ) → ( Image 𝑅 ‘ 𝐴 ) = ( 𝑅 “ 𝐴 ) ) |
5 | 1 4 | sylan | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅 “ 𝐴 ) ∈ 𝑊 ) → ( Image 𝑅 ‘ 𝐴 ) = ( 𝑅 “ 𝐴 ) ) |