Theorem feq12i

Description: Equality inference for functions. (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	feq12i.1	$$⊢F=G$$
	feq12i.2	$$⊢A=B$$
Assertion	feq12i	$$⊢F:A⟶C\leftrightarrow G:B⟶C$$

Proof

Step	Hyp	Ref	Expression
1		feq12i.1	$$⊢F=G$$
2		feq12i.2	$$⊢A=B$$
3		eqid	$$⊢C=C$$
4		feq123	$$⊢\left(F=G\wedge A=B\wedge C=C\right)\to \left(F:A⟶C\leftrightarrow G:B⟶C\right)$$
5	1 2 3 4	mp3an	$$⊢F:A⟶C\leftrightarrow G:B⟶C$$