This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrid ⊢ ( ( 𝐹 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 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )