Theorem feq2dd

Description: Equality deduction for functions. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	feq2dd.eq	$$⊢\phi \to A=B$$
	feq2dd.f	$$⊢\phi \to F:A⟶C$$
Assertion	feq2dd	$$⊢\phi \to F:B⟶C$$

Proof

Step	Hyp	Ref	Expression
1		feq2dd.eq	$$⊢\phi \to A=B$$
2		feq2dd.f	$$⊢\phi \to F:A⟶C$$
3	1	feq2d	$$⊢\phi \to \left(F:A⟶C\leftrightarrow F:B⟶C\right)$$
4	2 3	mpbid	$$⊢\phi \to F:B⟶C$$