Theorem feq123

Description: Equality theorem for functions. (Contributed by FL, 16-Nov-2008)

	Ref	Expression
Assertion	feq123	⊢ ( ( 𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐺 : 𝐶 ⟶ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → 𝐹 = 𝐺 )
2		simp2	⊢ ( ( 𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → 𝐴 = 𝐶 )
3		simp3	⊢ ( ( 𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → 𝐵 = 𝐷 )
4	1 2 3	feq123d	⊢ ( ( 𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐺 : 𝐶 ⟶ 𝐷 ) )