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 ) )