Theorem fvoveq1 5864

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

Assertion

Ref	Expression
fvoveq1	|- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )

Proof of Theorem fvoveq1

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( A = B -> A = B )
2	1	fvoveq1d 5863	1 |- ( A = B -> ( F ` ( A O C ) ) = ( F ` ( B O C ) ) )

Syntax hints:   -> wi 4   = wceq 1343   ` cfv 5187  (class class class)co 5841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  seq3val  10389  seqvalcd  10390  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  seq3shft2  10404  seq3f1olemqsum  10431  facp1  10639  serf0  11289  fsumrelem  11408  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  pcfac  12276  ennnfonelemj0  12330  ennnfonelemjn  12331  ennnfonelem0  12334  ennnfonelemp1  12335  ennnfonelemnn0  12351  nninfdclemcl  12377  nninfdclemp1  12379  nninfdc  12382  comet  13099  mulc1cncf  13176  cncfco  13178  mulcncflem  13190  mulcncf  13191  ivthinclemlopn  13214  ivthinclemuopn  13216  limcimolemlt  13233  limccoap  13247  eflt  13296  rpcxpef  13415