Metamath Proof Explorer

Theorem feq2i

Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011)

Ref Expression
Hypothesis feq2i.1 ⊢A=B
Assertion feq2i ⊢F:A⟶C↔F:B⟶C

Proof

Step Hyp Ref Expression
1 feq2i.1 ⊢A=B
2 feq2 ⊢A=B→F:A⟶C↔F:B⟶C
3 1 2 ax-mp ⊢F:A⟶C↔F:B⟶C