Metamath Proof Explorer

Theorem fvresi

Description: The value of a restricted identity function. (Contributed by NM, 19-May-2004)

Ref Expression
Assertion fvresi 
|- ( B e. A -> ( ( _I |` A ) ` B ) = B )

Proof

Step Hyp Ref Expression
1 fvres 
 |-  ( B e. A -> ( ( _I |` A ) ` B ) = ( _I ` B ) )
2 fvi 
 |-  ( B e. A -> ( _I ` B ) = B )
3 1 2 eqtrd 
 |-  ( B e. A -> ( ( _I |` A ) ` B ) = B )