Theorem feq23i

Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		feq23i.1	⊢ 𝐴 = 𝐶
2		feq23i.2	⊢ 𝐵 = 𝐷
3		feq23	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐷 ) )
4	1 2 3	mp2an	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐷 )