Theorem fvreseq

Description: Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994) (Proof shortened by AV, 4-Mar-2019)

	Ref	Expression
Assertion	fvreseq	$$⊢\left(\left(FFnA\wedge GFnA\right)\wedge B\subseteq A\right)\to \left({F\upharpoonright }_B={G\upharpoonright }_B\leftrightarrow \forall x\in BF\left(x\right)=G\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvreseq0	$$⊢\left(\left(FFnA\wedge GFnA\right)\wedge \left(B\subseteq A\wedge B\subseteq A\right)\right)\to \left({F\upharpoonright }_B={G\upharpoonright }_B\leftrightarrow \forall x\in BF\left(x\right)=G\left(x\right)\right)$$
2	1	anabsan2	$$⊢\left(\left(FFnA\wedge GFnA\right)\wedge B\subseteq A\right)\to \left({F\upharpoonright }_B={G\upharpoonright }_B\leftrightarrow \forall x\in BF\left(x\right)=G\left(x\right)\right)$$