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  19653  islmhm2  20921  coe1pwmul  22141  coe1sclmul  22144  evl1gsumadd  22221  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  mpomulcn  24734  mulc1cncf  24774  pcovalg  24888  ehl1eudisval  25297  ovolunlem1a  25373  ovolunlem1  25374  mbfi1fseq  25598  isibl  25642  isibl2  25643  cbvitg  25653  cbvitgv  25654  itgeqa  25691  dveflem  25859  dvferm1lem  25864  dvferm1  25865  dvferm2lem  25866  dvferm2  25867  dvlip  25874  c1lip1  25878  lhop1lem  25894  lhop1  25895  ftc1lem5  25923  vieta1lem2  26195  aalioulem3  26218  ulmshftlem  26274  ulmcaulem  26279  ulmcau  26280  ulmdvlem3  26287  rlimcnp  26851  scvxcvx  26872  jensenlem2  26874  lgamgulmlem2  26916  lgamgulmlem5  26919  lgamgulm2  26922  lgamcvglem  26926  lgamcvg2  26941  basellem4  26970  basellem5  26971  pcbcctr  27163  dchrisumlem3  27378  dchrmusumlema  27380  dchrmusum2  27381  dchrvmasumlem2  27385  dchrvmasumlema  27387  dchrvmasumiflem1  27388  dchrisum0lema  27401  dchrisum0lem1b  27402  dchrisum0lem2  27405  dchrisum0  27407  chpdifbndlem1  27440  selbergsb  27462  pntlemo  27494  crctcshwlkn0lem2  29714  crctcshwlkn0lem3  29715  crctcshlem4  29723  crctcsh  29727  clwwisshclwwslemlem  29915  lnolin  30656  lnoadd  30660  norm3adifi  31055  lnopl  31816  lnfnl  31833  lnopaddi  31873  lnfnaddi  31945  pfxlsw2ccat  32845  constrrtlc1  33695  constrrtcc  33698  lmatfval  33777  xrge0iifhom  33900  itgeq12dv  34290  signsply0  34515  revwlk  35085  snmlval  35291  iprodgam  35702  cbvitgvw2  36209  cbvitgdavw  36242  cbvitgdavw2  36258  knoppcnlem1  36454  knoppndvlem21  36493  matunitlindflem1  37583  poimirlem29  37616  poimirlem32  37619  itg2addnclem3  37640  ftc1cnnc  37659  ftc1anclem6  37665  ftc1anclem7  37666  geomcau  37726  lfli  39027  lfladd  39032  docavalN  41090  diaocN  41092  dihjatc  41384  dvh4dimat  41405  sticksstones10  42116  sticksstones12a  42118  irrapxlem3  42785  irrapxlem4  42786  pellexlem6  42795  rmxfval  42865  rmyfval  42866  hashnzfz  44282  hashnzfzclim  44284  caucvgbf  45458  cvgcaule  45460  climsuse  45579  mullimc  45587  climf  45593  mullimcf  45594  idlimc  45597  limcperiod  45599  clim2f  45607  limcleqr  45615  limclner  45622  climf2  45637  clim2f2  45641  fnlimabslt  45650  climuz  45715  fperdvper  45890  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnmul  45914  stoweidlem9  45980  wallispilem4  46039  wallispilem5  46040  dirkerval  46062  dirkerval2  46065  dirkertrigeqlem1  46069  dirkertrigeqlem2  46070  dirkertrigeq  46072  dirkercncflem2  46075  ovnhoi  46574  hspmbllem1  46597  digfval  48559  dignn0flhalflem2  48578  dfinito4  49463  ranfval  49576