Theorem eqfnfv2d2

Description: Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024)

	Ref	Expression
Hypotheses	eqfnfv2d2.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	eqfnfv2d2.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
	eqfnfv2d2.3	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	eqfnfv2d2.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
Assertion	eqfnfv2d2	⊢ ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqfnfv2d2.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		eqfnfv2d2.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3		eqfnfv2d2.3	⊢ ( 𝜑 → 𝐴 = 𝐵 )
4		eqfnfv2d2.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
5	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
6	3 5	jca	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
7	1 2	jca	⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) )
8		eqfnfv2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
9	7 8	syl	⊢ ( 𝜑 → ( 𝐹 = 𝐺 ↔ ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
10	6 9	mpbird	⊢ ( 𝜑 → 𝐹 = 𝐺 )