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

Metamath Proof Explorer

Theorem fveqeq2d

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

Ref Expression
Hypothesis fveqeq2d.1 ⊢ φ → A = B
Assertion fveqeq2d ⊢ φ → F ⁡ A = C ↔ F ⁡ B = C

Proof

Step Hyp Ref Expression
1 fveqeq2d.1 ⊢ φ → A = B
2 1 fveq2d ⊢ φ → F ⁡ A = F ⁡ B
3 2 eqeq1d ⊢ φ → F ⁡ A = C ↔ F ⁡ B = C