Theorem eqfnfvd

Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	eqfnfvd.1	$$⊢\phi \to FFnA$$
	eqfnfvd.2	$$⊢\phi \to GFnA$$
	eqfnfvd.3	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=G\left(x\right)$$
Assertion	eqfnfvd	$$⊢\phi \to F=G$$

Proof

Step	Hyp	Ref	Expression
1		eqfnfvd.1	$$⊢\phi \to FFnA$$
2		eqfnfvd.2	$$⊢\phi \to GFnA$$
3		eqfnfvd.3	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=G\left(x\right)$$
4	3	ralrimiva	$$⊢\phi \to \forall x\in AF\left(x\right)=G\left(x\right)$$
5		eqfnfv	$$⊢\left(FFnA\wedge GFnA\right)\to \left(F=G\leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)\right)$$
6	1 2 5	syl2anc	$$⊢\phi \to \left(F=G\leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)\right)$$
7	4 6	mpbird	$$⊢\phi \to F=G$$