Theorem feq12d

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

	Ref	Expression
Hypotheses	feq12d.1	|- ( ph -> F = G )
	feq12d.2	|- ( ph -> A = B )
Assertion	feq12d	|- ( ph -> ( F : A --> C <-> G : B --> C ) )

Proof

Step	Hyp	Ref	Expression
1		feq12d.1	|- ( ph -> F = G )
2		feq12d.2	|- ( ph -> A = B )
3	1	feq1d	|- ( ph -> ( F : A --> C <-> G : A --> C ) )
4	2	feq2d	|- ( ph -> ( G : A --> C <-> G : B --> C ) )
5	3 4	bitrd	|- ( ph -> ( F : A --> C <-> G : B --> C ) )