Theorem fvoveq1 5880

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

Assertion

Ref	Expression
fvoveq1	⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Proof of Theorem fvoveq1

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fvoveq1d 5879	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1349  ‘cfv 5200  (class class class)co 5857

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 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-rex 2455  df-v 2733  df-un 3126  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-iota 5162  df-fv 5208  df-ov 5860

This theorem is referenced by:  seq3val  10418  seqvalcd  10419  seqf  10421  seq3p1  10422  seqovcd  10423  seqp1cd  10426  seq3shft2  10433  seq3f1olemqsum  10460  facp1  10668  serf0  11319  fsumrelem  11438  mertenslemub  11501  mertenslemi1  11502  mertenslem2  11503  mertensabs  11504  pcfac  12306  ennnfonelemj0  12360  ennnfonelemjn  12361  ennnfonelem0  12364  ennnfonelemp1  12365  ennnfonelemnn0  12381  nninfdclemcl  12407  nninfdclemp1  12409  nninfdc  12412  mhmlin  12694  mhmlem  12811  mulginvcom  12840  mhmmulg  12856  comet  13378  mulc1cncf  13455  cncfco  13457  mulcncflem  13469  mulcncf  13470  ivthinclemlopn  13493  ivthinclemuopn  13495  limcimolemlt  13512  limccoap  13526  eflt  13575  rpcxpef  13694