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