Metamath Proof Explorer

Theorem eqfunfv

Description: Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011)

Ref Expression
Assertion eqfunfv ⊢ Fun ⁡ F ∧ Fun ⁡ G → F = G ↔ dom ⁡ F = dom ⁡ G ∧ ∀ x ∈ dom ⁡ F F ⁡ x = G ⁡ x

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
2 funfn ⊢ Fun ⁡ G ↔ G Fn dom ⁡ G
3 eqfnfv2 ⊢ F Fn dom ⁡ F ∧ G Fn dom ⁡ G → F = G ↔ dom ⁡ F = dom ⁡ G ∧ ∀ x ∈ dom ⁡ F F ⁡ x = G ⁡ x
4 1 2 3 syl2anb ⊢ Fun ⁡ F ∧ Fun ⁡ G → F = G ↔ dom ⁡ F = dom ⁡ G ∧ ∀ x ∈ dom ⁡ F F ⁡ x = G ⁡ x