Theorem bnj1536

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1536.1	$$⊢\phi \to FFnA$$
	bnj1536.2	$$⊢\phi \to GFnA$$
	bnj1536.3	$$⊢\phi \to B\subseteq A$$
	bnj1536.4	$$⊢\phi \to \forall x\in BF\left(x\right)=G\left(x\right)$$
Assertion	bnj1536	$$⊢\phi \to {F\upharpoonright }_B={G\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		bnj1536.1	$$⊢\phi \to FFnA$$
2		bnj1536.2	$$⊢\phi \to GFnA$$
3		bnj1536.3	$$⊢\phi \to B\subseteq A$$
4		bnj1536.4	$$⊢\phi \to \forall x\in BF\left(x\right)=G\left(x\right)$$
5		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)$$
6	1 2 3 5	syl21anc	$$⊢\phi \to \left({F\upharpoonright }_B={G\upharpoonright }_B\leftrightarrow \forall x\in BF\left(x\right)=G\left(x\right)\right)$$
7	4 6	mpbird	$$⊢\phi \to {F\upharpoonright }_B={G\upharpoonright }_B$$