Metamath Proof Explorer


Theorem fveqeq2

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

Ref Expression
Assertion fveqeq2 A=BFA=CFB=C

Proof

Step Hyp Ref Expression
1 id A=BA=B
2 1 fveqeq2d A=BFA=CFB=C