This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fveqres

Description: Equal values imply equal values in a restriction. (Contributed by NM, 13-Nov-1995)

Ref Expression
Assertion fveqres 
|- ( ( F ` A ) = ( G ` A ) -> ( ( F |` B ) ` A ) = ( ( G |` B ) ` A ) )

Proof

Step Hyp Ref Expression
1 fvres 
 |-  ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )
2 fvres 
 |-  ( A e. B -> ( ( G |` B ) ` A ) = ( G ` A ) )
3 1 2 eqeq12d 
 |-  ( A e. B -> ( ( ( F |` B ) ` A ) = ( ( G |` B ) ` A ) <-> ( F ` A ) = ( G ` A ) ) )
4 3 biimprd 
 |-  ( A e. B -> ( ( F ` A ) = ( G ` A ) -> ( ( F |` B ) ` A ) = ( ( G |` B ) ` A ) ) )
5 nfvres 
 |-  ( -. A e. B -> ( ( F |` B ) ` A ) = (/) )
6 nfvres 
 |-  ( -. A e. B -> ( ( G |` B ) ` A ) = (/) )
7 5 6 eqtr4d 
 |-  ( -. A e. B -> ( ( F |` B ) ` A ) = ( ( G |` B ) ` A ) )
8 7 a1d 
 |-  ( -. A e. B -> ( ( F ` A ) = ( G ` A ) -> ( ( F |` B ) ` A ) = ( ( G |` B ) ` A ) ) )
9 4 8 pm2.61i 
 |-  ( ( F ` A ) = ( G ` A ) -> ( ( F |` B ) ` A ) = ( ( G |` B ) ` A ) )