Theorem feq23d

Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013)

	Ref	Expression
Hypotheses	feq23d.1	⊢ ( 𝜑 → 𝐴 = 𝐶 )
	feq23d.2	⊢ ( 𝜑 → 𝐵 = 𝐷 )
Assertion	feq23d	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		feq23d.1	⊢ ( 𝜑 → 𝐴 = 𝐶 )
2		feq23d.2	⊢ ( 𝜑 → 𝐵 = 𝐷 )
3		eqidd	⊢ ( 𝜑 → 𝐹 = 𝐹 )
4	3 1 2	feq123d	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐷 ) )