Theorem eqfnfv2d2

Description: Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		eqfnfv2d2.1	$$⊢\phi \to FFnA$$
2		eqfnfv2d2.2	$$⊢\phi \to GFnB$$
3		eqfnfv2d2.3	$$⊢\phi \to A=B$$
4		eqfnfv2d2.4	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)=G\left(x\right)$$
5	4	ralrimiva	$$⊢\phi \to \forall x\in AF\left(x\right)=G\left(x\right)$$
6	3 5	jca	$$⊢\phi \to \left(A=B\wedge \forall x\in AF\left(x\right)=G\left(x\right)\right)$$
7	1 2	jca	$$⊢\phi \to \left(FFnA\wedge GFnB\right)$$
8		eqfnfv2	$$⊢\left(FFnA\wedge GFnB\right)\to \left(F=G\leftrightarrow \left(A=B\wedge \forall x\in AF\left(x\right)=G\left(x\right)\right)\right)$$
9	7 8	syl	$$⊢\phi \to \left(F=G\leftrightarrow \left(A=B\wedge \forall x\in AF\left(x\right)=G\left(x\right)\right)\right)$$
10	6 9	mpbird	$$⊢\phi \to F=G$$