Theorem fveqres

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

	Ref	Expression
Assertion	fveqres	$$⊢F\left(A\right)=G\left(A\right)\to \left({F\upharpoonright }_B\right)\left(A\right)=\left({G\upharpoonright }_B\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvres	$$⊢A\in B\to \left({F\upharpoonright }_B\right)\left(A\right)=F\left(A\right)$$
2		fvres	$$⊢A\in B\to \left({G\upharpoonright }_B\right)\left(A\right)=G\left(A\right)$$
3	1 2	eqeq12d	$$⊢A\in B\to \left(\left({F\upharpoonright }_B\right)\left(A\right)=\left({G\upharpoonright }_B\right)\left(A\right)\leftrightarrow F\left(A\right)=G\left(A\right)\right)$$
4	3	biimprd	$$⊢A\in B\to \left(F\left(A\right)=G\left(A\right)\to \left({F\upharpoonright }_B\right)\left(A\right)=\left({G\upharpoonright }_B\right)\left(A\right)\right)$$
5		nfvres	$$⊢\neg A\in B\to \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing$$
6		nfvres	$$⊢\neg A\in B\to \left({G\upharpoonright }_B\right)\left(A\right)=\varnothing$$
7	5 6	eqtr4d	$$⊢\neg A\in B\to \left({F\upharpoonright }_B\right)\left(A\right)=\left({G\upharpoonright }_B\right)\left(A\right)$$
8	7	a1d	$$⊢\neg A\in B\to \left(F\left(A\right)=G\left(A\right)\to \left({F\upharpoonright }_B\right)\left(A\right)=\left({G\upharpoonright }_B\right)\left(A\right)\right)$$
9	4 8	pm2.61i	$$⊢F\left(A\right)=G\left(A\right)\to \left({F\upharpoonright }_B\right)\left(A\right)=\left({G\upharpoonright }_B\right)\left(A\right)$$