Theorem fvoveq1 6040

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 6039. (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 6039	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1397  ‘cfv 5326  (class class class)co 6017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  fldiv4lem1div2  10566  seq3val  10721  seqvalcd  10722  seqf  10725  seq3p1  10726  seqovcd  10728  seqp1cd  10731  seq3shft2  10742  seqshft2g  10743  seq3f1olemqsum  10774  seqhomog  10791  facp1  10991  lsw0  11160  ccatval1  11173  ccatval2  11174  ccatalpha  11189  swrdfv  11233  serf0  11912  fsumrelem  12031  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  bitsfval  12502  pcfac  12922  ennnfonelemj0  13021  ennnfonelemjn  13022  ennnfonelem0  13025  ennnfonelemp1  13026  ennnfonelemnn0  13042  nninfdclemcl  13068  nninfdclemp1  13070  nninfdc  13073  imasaddvallemg  13397  mhmlin  13549  mhmlem  13700  mulginvcom  13733  mhmmulg  13749  ghmlin  13834  comet  15222  mulc1cncf  15312  cncfco  15314  mulcncflem  15330  mulcncf  15331  ivthinclemlopn  15359  ivthinclemuopn  15361  limcimolemlt  15387  limccoap  15401  dvply1  15488  dvply2g  15489  eflt  15498  rpcxpef  15617  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  wkslem1  16170  uspgr2wlkeq  16215  clwwlkccatlem  16250  clwwlkext2edg  16272  clwwlknonex2lem2  16288  eupthseg  16302