Theorem fvoveq1d 7371

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6482  (class class class)co 7349

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  fvoveq1  7372  imbrov2fvoveq  7374  hashfzp1  14338  pfxfvlsw  14601  swrdswrd  14611  revrev  14673  cshwidx0mod  14711  2cshw  14719  lswcshw  14721  cshweqrep  14727  cshimadifsn0  14737  lswco  14746  cau3lem  15262  clim  15401  rlim  15402  rlim2  15403  clim2  15411  rlimclim  15453  climrlim2  15454  climshftlem  15481  rlimcn3  15497  climcn2  15500  subcn2  15502  isercoll  15575  climcau  15578  caurcvg2  15585  caucvgb  15587  iseralt  15592  climcndslem1  15756  smumullem  16403  prmreclem4  16831  cshwsidrepsw  17005  efgredlem  19626  islmhm2  20942  coe1pwmul  22163  coe1sclmul  22166  evl1gsumadd  22243  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  mpomulcn  24756  mulc1cncf  24796  pcovalg  24910  ehl1eudisval  25319  ovolunlem1a  25395  ovolunlem1  25396  mbfi1fseq  25620  isibl  25664  isibl2  25665  cbvitg  25675  cbvitgv  25676  itgeqa  25713  dveflem  25881  dvferm1lem  25886  dvferm1  25887  dvferm2lem  25888  dvferm2  25889  dvlip  25896  c1lip1  25900  lhop1lem  25916  lhop1  25917  ftc1lem5  25945  vieta1lem2  26217  aalioulem3  26240  ulmshftlem  26296  ulmcaulem  26301  ulmcau  26302  ulmdvlem3  26309  rlimcnp  26873  scvxcvx  26894  jensenlem2  26896  lgamgulmlem2  26938  lgamgulmlem5  26941  lgamgulm2  26944  lgamcvglem  26948  lgamcvg2  26963  basellem4  26992  basellem5  26993  pcbcctr  27185  dchrisumlem3  27400  dchrmusumlema  27402  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumlema  27409  dchrvmasumiflem1  27410  dchrisum0lema  27423  dchrisum0lem1b  27424  dchrisum0lem2  27427  dchrisum0  27429  chpdifbndlem1  27462  selbergsb  27484  pntlemo  27516  crctcshwlkn0lem2  29756  crctcshwlkn0lem3  29757  crctcshlem4  29765  crctcsh  29769  clwwisshclwwslemlem  29957  lnolin  30698  lnoadd  30702  norm3adifi  31097  lnopl  31858  lnfnl  31875  lnopaddi  31915  lnfnaddi  31987  pfxlsw2ccat  32892  constrrtlc1  33699  constrrtcc  33702  lmatfval  33781  xrge0iifhom  33904  itgeq12dv  34294  signsply0  34519  revwlk  35098  snmlval  35304  iprodgam  35715  cbvitgvw2  36222  cbvitgdavw  36255  cbvitgdavw2  36271  knoppcnlem1  36467  knoppndvlem21  36506  matunitlindflem1  37596  poimirlem29  37629  poimirlem32  37632  itg2addnclem3  37653  ftc1cnnc  37672  ftc1anclem6  37678  ftc1anclem7  37679  geomcau  37739  lfli  39040  lfladd  39045  docavalN  41102  diaocN  41104  dihjatc  41396  dvh4dimat  41417  sticksstones10  42128  sticksstones12a  42130  irrapxlem3  42797  irrapxlem4  42798  pellexlem6  42807  rmxfval  42877  rmyfval  42878  hashnzfz  44293  hashnzfzclim  44295  caucvgbf  45468  cvgcaule  45470  climsuse  45589  mullimc  45597  climf  45603  mullimcf  45604  idlimc  45607  limcperiod  45609  clim2f  45617  limcleqr  45625  limclner  45632  climf2  45647  clim2f2  45651  fnlimabslt  45660  climuz  45725  fperdvper  45900  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  dvnmul  45924  stoweidlem9  45990  wallispilem4  46049  wallispilem5  46050  dirkerval  46072  dirkerval2  46075  dirkertrigeqlem1  46079  dirkertrigeqlem2  46080  dirkertrigeq  46082  dirkercncflem2  46085  ovnhoi  46584  hspmbllem1  46607  digfval  48582  dignn0flhalflem2  48601  dfinito4  49486  ranfval  49599