Theorem eqfunfv

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 𝐹 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )