Theorem fvoveq1d 7277

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

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6418  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  fvoveq1  7278  imbrov2fvoveq  7280  hashfzp1  14074  pfxfvlsw  14336  swrdswrd  14346  revrev  14408  cshwidx0mod  14446  2cshw  14454  lswcshw  14456  cshweqrep  14462  cshimadifsn0  14471  lswco  14480  cau3lem  14994  clim  15131  rlim  15132  rlim2  15133  clim2  15141  rlimclim  15183  climrlim2  15184  climshftlem  15211  rlimcn3  15227  climcn2  15230  subcn2  15232  isercoll  15307  climcau  15310  caurcvg2  15317  caucvgb  15319  iseralt  15324  climcndslem1  15489  smumullem  16127  prmreclem4  16548  cshwsidrepsw  16723  efgredlem  19268  islmhm2  20215  coe1pwmul  21360  coe1sclmul  21363  evl1gsumadd  21434  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  mulc1cncf  23974  pcovalg  24081  ehl1eudisval  24490  ovolunlem1a  24565  ovolunlem1  24566  mbfi1fseq  24791  isibl  24835  isibl2  24836  cbvitg  24845  itgeqa  24883  dveflem  25048  dvferm1lem  25053  dvferm1  25054  dvferm2lem  25055  dvferm2  25056  dvlip  25062  c1lip1  25066  lhop1lem  25082  lhop1  25083  ftc1lem5  25109  vieta1lem2  25376  aalioulem3  25399  ulmshftlem  25453  ulmcaulem  25458  ulmcau  25459  ulmdvlem3  25466  rlimcnp  26020  scvxcvx  26040  jensenlem2  26042  lgamgulmlem2  26084  lgamgulmlem5  26087  lgamgulm2  26090  lgamcvglem  26094  lgamcvg2  26109  basellem4  26138  basellem5  26139  pcbcctr  26329  dchrisumlem3  26544  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumlema  26553  dchrvmasumiflem1  26554  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem2  26571  dchrisum0  26573  chpdifbndlem1  26606  selbergsb  26628  pntlemo  26660  crctcshwlkn0lem2  28077  crctcshwlkn0lem3  28078  crctcshlem4  28086  crctcsh  28090  clwwisshclwwslemlem  28278  lnolin  29017  lnoadd  29021  norm3adifi  29416  lnopl  30177  lnfnl  30194  lnopaddi  30234  lnfnaddi  30306  pfxlsw2ccat  31126  lmatfval  31666  xrge0iifhom  31789  itgeq12dv  32193  signsply0  32430  revwlk  32986  snmlval  33193  iprodgam  33614  knoppcnlem1  34600  knoppndvlem21  34639  matunitlindflem1  35700  poimirlem29  35733  poimirlem32  35736  itg2addnclem3  35757  ftc1cnnc  35776  ftc1anclem6  35782  ftc1anclem7  35783  geomcau  35844  lfli  37002  lfladd  37007  docavalN  39064  diaocN  39066  dihjatc  39358  dvh4dimat  39379  sticksstones10  40039  sticksstones12a  40041  irrapxlem3  40562  irrapxlem4  40563  pellexlem6  40572  rmxfval  40642  rmyfval  40643  hashnzfz  41827  hashnzfzclim  41829  climsuse  43039  mullimc  43047  climf  43053  mullimcf  43054  idlimc  43057  limcperiod  43059  clim2f  43067  limcleqr  43075  limclner  43082  climf2  43097  clim2f2  43101  fnlimabslt  43110  climuz  43175  fperdvper  43350  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  stoweidlem9  43440  wallispilem4  43499  wallispilem5  43500  dirkerval  43522  dirkerval2  43525  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeq  43532  dirkercncflem2  43535  ovnhoi  44031  hspmbllem1  44054  digfval  45831  dignn0flhalflem2  45850