Theorem fvoveq1 6098

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

Syntax hints:   → wi 4   = wceq 1402  ‘cfv 5372  (class class class)co 6075

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  fldiv4lem1div2  10720  seq3val  10875  seqvalcd  10876  seqf  10879  seq3p1  10880  seqovcd  10882  seqp1cd  10885  seq3shft2  10896  seqshft2g  10897  seq3f1olemqsum  10928  seqhomog  10945  facp1  11146  lsw0  11330  ccatval1  11343  ccatval2  11344  ccatalpha  11359  swrdfv  11403  serf0  12096  fsumrelem  12216  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  bitsfval  12687  pcfac  13107  ennnfonelemj0  13270  ennnfonelemjn  13271  ennnfonelem0  13274  ennnfonelemp1  13275  ennnfonelemnn0  13291  nninfdclemcl  13317  nninfdclemp1  13319  nninfdc  13322  imasaddvallemg  13613  mhmlin  13751  mhmlem  13894  mulginvcom  13927  mhmmulg  13943  ghmlin  14028  comet  15523  mulc1cncf  15613  cncfco  15615  mulcncflem  15631  mulcncf  15632  ivthinclemlopn  15660  ivthinclemuopn  15662  limcimolemlt  15688  limccoap  15702  dvply1  15789  dvply2g  15790  eflt  15799  rpcxpef  15919  pellexlem3  16007  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  wkslem1  16475  uspgr2wlkeq  16520  clwwlkccatlem  16555  clwwlkext2edg  16577  clwwlknonex2lem2  16593  eupthseg  16607  eupth2lem3fi  16631  depindlem1  16661  depindlem2  16662  depindlem3  16663