This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem feq2i

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

Ref Expression
Hypothesis feq2i.1 ⊢ 𝐴 = 𝐵
Assertion feq2i ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ 𝐹 : 𝐵 ⟶ 𝐶 )

Proof

Step Hyp Ref Expression
1 feq2i.1 ⊢ 𝐴 = 𝐵
2 feq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ 𝐹 : 𝐵 ⟶ 𝐶 ) )
3 1 2 ax-mp ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ 𝐹 : 𝐵 ⟶ 𝐶 )