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	⊢ Ⅎ 𝑥 𝐹
	eqfnfv2f.2	⊢ Ⅎ 𝑥 𝐺
Assertion	eqfnfv2f	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqfnfv2f.1	⊢ Ⅎ 𝑥 𝐹
2		eqfnfv2f.2	⊢ Ⅎ 𝑥 𝐺
3		eqfnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
4		nfcv	⊢ Ⅎ 𝑥 𝑧
5	1 4	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
6	2 4	nffv	⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑧 )
7	5 6	nfeq	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 )
8		nfv	⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 )
9		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
10		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑥 ) )
11	9 10	eqeq12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
12	7 8 11	cbvralw	⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
13	3 12	bitrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )