Theorem fvoveq1d 7391

Description: Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)

Hypothesis

Ref	Expression
fvoveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

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

Proof of Theorem fvoveq1d

Step	Hyp	Ref	Expression
1		fvoveq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	oveq1d 7384	. 2 ⊢ (𝜑 → (𝐴𝑂𝐶) = (𝐵𝑂𝐶))
3	2	fveq2d 6844	1 ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6499  (class class class)co 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  fvoveq1  7392  imbrov2fvoveq  7394  hashfzp1  14372  pfxfvlsw  14636  swrdswrd  14646  revrev  14708  cshwidx0mod  14746  2cshw  14754  lswcshw  14756  cshweqrep  14762  cshimadifsn0  14772  lswco  14781  cau3lem  15297  clim  15436  rlim  15437  rlim2  15438  clim2  15446  rlimclim  15488  climrlim2  15489  climshftlem  15516  rlimcn3  15532  climcn2  15535  subcn2  15537  isercoll  15610  climcau  15613  caurcvg2  15620  caucvgb  15622  iseralt  15627  climcndslem1  15791  smumullem  16438  prmreclem4  16866  cshwsidrepsw  17040  efgredlem  19661  islmhm2  20977  coe1pwmul  22198  coe1sclmul  22201  evl1gsumadd  22278  chfacfscmulgsum  22780  chfacfpmmulgsum  22784  mpomulcn  24791  mulc1cncf  24831  pcovalg  24945  ehl1eudisval  25354  ovolunlem1a  25430  ovolunlem1  25431  mbfi1fseq  25655  isibl  25699  isibl2  25700  cbvitg  25710  cbvitgv  25711  itgeqa  25748  dveflem  25916  dvferm1lem  25921  dvferm1  25922  dvferm2lem  25923  dvferm2  25924  dvlip  25931  c1lip1  25935  lhop1lem  25951  lhop1  25952  ftc1lem5  25980  vieta1lem2  26252  aalioulem3  26275  ulmshftlem  26331  ulmcaulem  26336  ulmcau  26337  ulmdvlem3  26344  rlimcnp  26908  scvxcvx  26929  jensenlem2  26931  lgamgulmlem2  26973  lgamgulmlem5  26976  lgamgulm2  26979  lgamcvglem  26983  lgamcvg2  26998  basellem4  27027  basellem5  27028  pcbcctr  27220  dchrisumlem3  27435  dchrmusumlema  27437  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumlema  27444  dchrvmasumiflem1  27445  dchrisum0lema  27458  dchrisum0lem1b  27459  dchrisum0lem2  27462  dchrisum0  27464  chpdifbndlem1  27497  selbergsb  27519  pntlemo  27551  crctcshwlkn0lem2  29791  crctcshwlkn0lem3  29792  crctcshlem4  29800  crctcsh  29804  clwwisshclwwslemlem  29992  lnolin  30733  lnoadd  30737  norm3adifi  31132  lnopl  31893  lnfnl  31910  lnopaddi  31950  lnfnaddi  32022  pfxlsw2ccat  32922  constrrtlc1  33715  constrrtcc  33718  lmatfval  33797  xrge0iifhom  33920  itgeq12dv  34310  signsply0  34535  revwlk  35105  snmlval  35311  iprodgam  35722  cbvitgvw2  36229  cbvitgdavw  36262  cbvitgdavw2  36278  knoppcnlem1  36474  knoppndvlem21  36513  matunitlindflem1  37603  poimirlem29  37636  poimirlem32  37639  itg2addnclem3  37660  ftc1cnnc  37679  ftc1anclem6  37685  ftc1anclem7  37686  geomcau  37746  lfli  39047  lfladd  39052  docavalN  41110  diaocN  41112  dihjatc  41404  dvh4dimat  41425  sticksstones10  42136  sticksstones12a  42138  irrapxlem3  42805  irrapxlem4  42806  pellexlem6  42815  rmxfval  42885  rmyfval  42886  hashnzfz  44302  hashnzfzclim  44304  caucvgbf  45478  cvgcaule  45480  climsuse  45599  mullimc  45607  climf  45613  mullimcf  45614  idlimc  45617  limcperiod  45619  clim2f  45627  limcleqr  45635  limclner  45642  climf2  45657  clim2f2  45661  fnlimabslt  45670  climuz  45735  fperdvper  45910  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  stoweidlem9  46000  wallispilem4  46059  wallispilem5  46060  dirkerval  46082  dirkerval2  46085  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkertrigeq  46092  dirkercncflem2  46095  ovnhoi  46594  hspmbllem1  46617  digfval  48579  dignn0flhalflem2  48598  dfinito4  49483  ranfval  49596