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

Metamath Proof Explorer

Theorem funeqi

Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypothesis funeqi.1 ⊢ A = B
Assertion funeqi ⊢ Fun ⁡ A ↔ Fun ⁡ B

Proof

Step Hyp Ref Expression
1 funeqi.1 ⊢ A = B
2 funeq ⊢ A = B → Fun ⁡ A ↔ Fun ⁡ B
3 1 2 ax-mp ⊢ Fun ⁡ A ↔ Fun ⁡ B