Theorem feq123

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

	Ref	Expression
Assertion	feq123	$$⊢\left(F=G\wedge A=C\wedge B=D\right)\to \left(F:A⟶B\leftrightarrow G:C⟶D\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(F=G\wedge A=C\wedge B=D\right)\to F=G$$
2		simp2	$$⊢\left(F=G\wedge A=C\wedge B=D\right)\to A=C$$
3		simp3	$$⊢\left(F=G\wedge A=C\wedge B=D\right)\to B=D$$
4	1 2 3	feq123d	$$⊢\left(F=G\wedge A=C\wedge B=D\right)\to \left(F:A⟶B\leftrightarrow G:C⟶D\right)$$