Metamath Proof Explorer

Theorem feq2

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion feq2 ⊢A=B→F:A⟶C↔F:B⟶C

Proof

Step Hyp Ref Expression
1 fneq2 ⊢A=B→FFnA↔FFnB
2 1 anbi1d ⊢A=B→FFnA∧ran⁡F⊆C↔FFnB∧ran⁡F⊆C
3 df-f ⊢F:A⟶C↔FFnA∧ran⁡F⊆C
4 df-f ⊢F:B⟶C↔FFnB∧ran⁡F⊆C
5 2 3 4 3bitr4g ⊢A=B→F:A⟶C↔F:B⟶C