Theorem fvoveq1d 7378

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 7371	. 2 ⊢ (𝜑 → (𝐴𝑂𝐶) = (𝐵𝑂𝐶))
3	2	fveq2d 6836	1 ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6490  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  fvoveq1  7379  imbrov2fvoveq  7381  hashfzp1  14352  pfxfvlsw  14616  swrdswrd  14626  revrev  14688  cshwidx0mod  14726  2cshw  14734  lswcshw  14736  cshweqrep  14742  cshimadifsn0  14751  lswco  14760  cau3lem  15276  clim  15415  rlim  15416  rlim2  15417  clim2  15425  rlimclim  15467  climrlim2  15468  climshftlem  15495  rlimcn3  15511  climcn2  15514  subcn2  15516  isercoll  15589  climcau  15592  caurcvg2  15599  caucvgb  15601  iseralt  15606  climcndslem1  15770  smumullem  16417  prmreclem4  16845  cshwsidrepsw  17019  efgredlem  19674  islmhm2  20988  coe1pwmul  22219  coe1sclmul  22222  evl1gsumadd  22300  chfacfscmulgsum  22802  chfacfpmmulgsum  22806  mpomulcn  24812  mulc1cncf  24852  pcovalg  24966  ehl1eudisval  25375  ovolunlem1a  25451  ovolunlem1  25452  mbfi1fseq  25676  isibl  25720  isibl2  25721  cbvitg  25731  cbvitgv  25732  itgeqa  25769  dveflem  25937  dvferm1lem  25942  dvferm1  25943  dvferm2lem  25944  dvferm2  25945  dvlip  25952  c1lip1  25956  lhop1lem  25972  lhop1  25973  ftc1lem5  26001  vieta1lem2  26273  aalioulem3  26296  ulmshftlem  26352  ulmcaulem  26357  ulmcau  26358  ulmdvlem3  26365  rlimcnp  26929  scvxcvx  26950  jensenlem2  26952  lgamgulmlem2  26994  lgamgulmlem5  26997  lgamgulm2  27000  lgamcvglem  27004  lgamcvg2  27019  basellem4  27048  basellem5  27049  pcbcctr  27241  dchrisumlem3  27456  dchrmusumlema  27458  dchrmusum2  27459  dchrvmasumlem2  27463  dchrvmasumlema  27465  dchrvmasumiflem1  27466  dchrisum0lema  27479  dchrisum0lem1b  27480  dchrisum0lem2  27483  dchrisum0  27485  chpdifbndlem1  27518  selbergsb  27540  pntlemo  27572  crctcshwlkn0lem2  29833  crctcshwlkn0lem3  29834  crctcshlem4  29842  crctcsh  29846  clwwisshclwwslemlem  30037  lnolin  30778  lnoadd  30782  norm3adifi  31177  lnopl  31938  lnfnl  31955  lnopaddi  31995  lnfnaddi  32067  pfxlsw2ccat  32981  extvfval  33646  mplvrpmrhm  33661  constrrtlc1  33838  constrrtcc  33841  lmatfval  33920  xrge0iifhom  34043  itgeq12dv  34432  signsply0  34657  revwlk  35268  snmlval  35474  iprodgam  35885  cbvitgvw2  36391  cbvitgdavw  36424  cbvitgdavw2  36440  knoppcnlem1  36636  knoppndvlem21  36675  matunitlindflem1  37756  poimirlem29  37789  poimirlem32  37792  itg2addnclem3  37813  ftc1cnnc  37832  ftc1anclem6  37838  ftc1anclem7  37839  geomcau  37899  lfli  39260  lfladd  39265  docavalN  41322  diaocN  41324  dihjatc  41616  dvh4dimat  41637  sticksstones10  42348  sticksstones12a  42350  irrapxlem3  43008  irrapxlem4  43009  pellexlem6  43018  rmxfval  43088  rmyfval  43089  hashnzfz  44503  hashnzfzclim  44505  caucvgbf  45675  cvgcaule  45677  climsuse  45796  mullimc  45804  climf  45810  mullimcf  45811  idlimc  45814  limcperiod  45816  clim2f  45822  limcleqr  45830  limclner  45837  climf2  45852  clim2f2  45856  fnlimabslt  45865  climuz  45930  fperdvper  46105  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnmul  46129  stoweidlem9  46195  wallispilem4  46254  wallispilem5  46255  dirkerval  46277  dirkerval2  46280  dirkertrigeqlem1  46284  dirkertrigeqlem2  46285  dirkertrigeq  46287  dirkercncflem2  46290  ovnhoi  46789  hspmbllem1  46812  digfval  48785  dignn0flhalflem2  48804  dfinito4  49688  ranfval  49801