This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011)
|
|
Ref |
Expression |
|
Assertion |
eqfunfv |
⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( 𝐹 = 𝐺 ↔ ( dom 𝐹 = dom 𝐺 ∧ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funfn |
⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 ) |
| 2 |
|
funfn |
⊢ ( Fun 𝐺 ↔ 𝐺 Fn dom 𝐺 ) |
| 3 |
|
eqfnfv2 |
⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺 ) → ( 𝐹 = 𝐺 ↔ ( dom 𝐹 = dom 𝐺 ∧ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) |
| 4 |
1 2 3
|
syl2anb |
⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( 𝐹 = 𝐺 ↔ ( dom 𝐹 = dom 𝐺 ∧ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ) |