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