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

Metamath Proof Explorer

Theorem fveqeq2

Description: Equality deduction for function value. (Contributed by BJ, 31-Aug-2022)

Ref Expression
Assertion fveqeq2 ⊢ A = B → F ⁡ A = C ↔ F ⁡ B = C

Proof

Step Hyp Ref Expression
1 id ⊢ A = B → A = B
2 1 fveqeq2d ⊢ A = B → F ⁡ A = C ↔ F ⁡ B = C