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 ⊢ F Fn A ∧ G Fn B → F = G ↔ A = B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x

Proof

Step Hyp Ref Expression
1 dmeq ⊢ F = G → dom ⁡ F = dom ⁡ G
2 fndm ⊢ F Fn A → dom ⁡ F = A
3 fndm ⊢ G Fn B → dom ⁡ G = B
4 2 3 eqeqan12d ⊢ F Fn A ∧ G Fn B → dom ⁡ F = dom ⁡ G ↔ A = B
5 1 4 imbitrid ⊢ F Fn A ∧ G Fn B → F = G → A = B
6 5 pm4.71rd ⊢ F Fn A ∧ G Fn B → F = G ↔ A = B ∧ F = G
7 fneq2 ⊢ A = B → G Fn A ↔ G Fn B
8 7 biimparc ⊢ G Fn B ∧ A = B → G Fn A
9 eqfnfv ⊢ F Fn A ∧ G Fn A → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
10 8 9 sylan2 ⊢ F Fn A ∧ G Fn B ∧ A = B → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
11 10 anassrs ⊢ F Fn A ∧ G Fn B ∧ A = B → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
12 11 pm5.32da ⊢ F Fn A ∧ G Fn B → A = B ∧ F = G ↔ A = B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x
13 6 12 bitrd ⊢ F Fn A ∧ G Fn B → F = G ↔ A = B ∧ ∀ x ∈ A F ⁡ x = G ⁡ x