Theorem feq1dd

Description: Equality deduction for functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	feq1dd.eq	|- ( ph -> F = G )
	feq1dd.f	|- ( ph -> F : A --> B )
Assertion	feq1dd	|- ( ph -> G : A --> B )

Proof

Step	Hyp	Ref	Expression
1		feq1dd.eq	|- ( ph -> F = G )
2		feq1dd.f	|- ( ph -> F : A --> B )
3	1	feq1d	|- ( ph -> ( F : A --> B <-> G : A --> B ) )
4	2 3	mpbid	|- ( ph -> G : A --> B )