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 
|- ( ( A e. V /\ ( R " A ) e. W ) -> ( Image R ` A ) = ( R " A ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 imaeq2 
 |-  ( x = A -> ( R " x ) = ( R " A ) )
3 imageval 
 |-  Image R = ( x e. _V |-> ( R " x ) )
4 2 3 fvmptg 
 |-  ( ( A e. _V /\ ( R " A ) e. W ) -> ( Image R ` A ) = ( R " A ) )
5 1 4 sylan 
 |-  ( ( A e. V /\ ( R " A ) e. W ) -> ( Image R ` A ) = ( R " A ) )