Theorem eqfnfv2f

Description: Equality of functions is determined by their values. Special case of Exercise 4 of TakeutiZaring p. 28 (with domain equality omitted). This version of eqfnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004)

	Ref	Expression
Hypotheses	eqfnfv2f.1	$$⊢\underset{\_}{Ⅎ}xF$$
	eqfnfv2f.2	$$⊢\underset{\_}{Ⅎ}xG$$
Assertion	eqfnfv2f	$$⊢\left(FFnA\wedge GFnA\right)\to \left(F=G\leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqfnfv2f.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		eqfnfv2f.2	$$⊢\underset{\_}{Ⅎ}xG$$
3		eqfnfv	$$⊢\left(FFnA\wedge GFnA\right)\to \left(F=G\leftrightarrow \forall z\in AF\left(z\right)=G\left(z\right)\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
5	1 4	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z\right)$$
6	2 4	nffv	$$⊢\underset{\_}{Ⅎ}xG\left(z\right)$$
7	5 6	nfeq	$$⊢ℲxF\left(z\right)=G\left(z\right)$$
8		nfv	$$⊢ℲzF\left(x\right)=G\left(x\right)$$
9		fveq2	$$⊢z=x\to F\left(z\right)=F\left(x\right)$$
10		fveq2	$$⊢z=x\to G\left(z\right)=G\left(x\right)$$
11	9 10	eqeq12d	$$⊢z=x\to \left(F\left(z\right)=G\left(z\right)\leftrightarrow F\left(x\right)=G\left(x\right)\right)$$
12	7 8 11	cbvralw	$$⊢\forall z\in AF\left(z\right)=G\left(z\right)\leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)$$
13	3 12	bitrdi	$$⊢\left(FFnA\wedge GFnA\right)\to \left(F=G\leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)\right)$$