Theorem eqfnfv2

Description: Equality of functions is determined by their values. Exercise 4 of TakeutiZaring p. 28. (Contributed by NM, 3-Aug-1994) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	eqfnfv2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmeq	⊢ ( 𝐹 = 𝐺 → dom 𝐹 = dom 𝐺 )
2		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
3		fndm	⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
4	2 3	eqeqan12d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( dom 𝐹 = dom 𝐺 ↔ 𝐴 = 𝐵 ) )
5	1 4	syl5ib	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 → 𝐴 = 𝐵 ) )
6	5	pm4.71rd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) ) )
7		fneq2	⊢ ( 𝐴 = 𝐵 → ( 𝐺 Fn 𝐴 ↔ 𝐺 Fn 𝐵 ) )
8	7	biimparc	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐴 = 𝐵 ) → 𝐺 Fn 𝐴 )
9		eqfnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
10	8 9	sylan2	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐺 Fn 𝐵 ∧ 𝐴 = 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
11	10	anassrs	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ 𝐴 = 𝐵 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
12	11	pm5.32da	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) ↔ ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
13	6 12	bitrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )