Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d . (Contributed by AV, 23Jul2022)
Ref  Expression  

Assertion  fvoveq1   ( A = B > ( F ` ( A O C ) ) = ( F ` ( B O C ) ) ) 
Step  Hyp  Ref  Expression 

1  id   ( A = B > A = B ) 

2  1  fvoveq1d   ( A = B > ( F ` ( A O C ) ) = ( F ` ( B O C ) ) ) 