Metamath Proof Explorer


Theorem fvoveq1

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d . (Contributed by AV, 23-Jul-2022)

Ref Expression
Assertion fvoveq1 A = B F A O C = F B O C

Proof

Step Hyp Ref Expression
1 id A = B A = B
2 1 fvoveq1d A = B F A O C = F B O C