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 AVRAW𝖨𝗆𝖺𝗀𝖾RA=RA

Proof

Step Hyp Ref Expression
1 elex AVAV
2 imaeq2 x=ARx=RA
3 imageval 𝖨𝗆𝖺𝗀𝖾R=xVRx
4 2 3 fvmptg AVRAW𝖨𝗆𝖺𝗀𝖾RA=RA
5 1 4 sylan AVRAW𝖨𝗆𝖺𝗀𝖾RA=RA