Theorem fvoveq1d 7383

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6493  (class class class)co 7361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  fvoveq1  7384  imbrov2fvoveq  7386  hashfzp1  14387  pfxfvlsw  14651  swrdswrd  14661  revrev  14723  cshwidx0mod  14761  2cshw  14769  lswcshw  14771  cshweqrep  14777  cshimadifsn0  14786  lswco  14795  cau3lem  15311  clim  15450  rlim  15451  rlim2  15452  clim2  15460  rlimclim  15502  climrlim2  15503  climshftlem  15530  rlimcn3  15546  climcn2  15549  subcn2  15551  isercoll  15624  climcau  15627  caurcvg2  15634  caucvgb  15636  iseralt  15641  climcndslem1  15808  smumullem  16455  prmreclem4  16884  cshwsidrepsw  17058  efgredlem  19716  islmhm2  21028  coe1pwmul  22257  coe1sclmul  22260  evl1gsumadd  22336  chfacfscmulgsum  22838  chfacfpmmulgsum  22842  mpomulcn  24847  mulc1cncf  24885  pcovalg  24992  ehl1eudisval  25401  ovolunlem1a  25476  ovolunlem1  25477  mbfi1fseq  25701  isibl  25745  isibl2  25746  cbvitg  25756  cbvitgv  25757  itgeqa  25794  dveflem  25959  dvferm1lem  25964  dvferm1  25965  dvferm2lem  25966  dvferm2  25967  dvlip  25973  c1lip1  25977  lhop1lem  25993  lhop1  25994  ftc1lem5  26020  vieta1lem2  26291  aalioulem3  26314  ulmshftlem  26370  ulmcaulem  26375  ulmcau  26376  ulmdvlem3  26383  rlimcnp  26945  scvxcvx  26966  jensenlem2  26968  lgamgulmlem2  27010  lgamgulmlem5  27013  lgamgulm2  27016  lgamcvglem  27020  lgamcvg2  27035  basellem4  27064  basellem5  27065  pcbcctr  27256  dchrisumlem3  27471  dchrmusumlema  27473  dchrmusum2  27474  dchrvmasumlem2  27478  dchrvmasumlema  27480  dchrvmasumiflem1  27481  dchrisum0lema  27494  dchrisum0lem1b  27495  dchrisum0lem2  27498  dchrisum0  27500  chpdifbndlem1  27533  selbergsb  27555  pntlemo  27587  crctcshwlkn0lem2  29897  crctcshwlkn0lem3  29898  crctcshlem4  29906  crctcsh  29910  clwwisshclwwslemlem  30101  lnolin  30843  lnoadd  30847  norm3adifi  31242  lnopl  32003  lnfnl  32020  lnopaddi  32060  lnfnaddi  32132  pfxlsw2ccat  33028  extvfval  33694  mplvrpmrhm  33709  constrrtlc1  33895  constrrtcc  33898  lmatfval  33977  xrge0iifhom  34100  itgeq12dv  34489  signsply0  34714  revwlk  35326  snmlval  35532  iprodgam  35943  cbvitgvw2  36449  cbvitgdavw  36482  cbvitgdavw2  36498  knoppcnlem1  36772  knoppndvlem21  36811  matunitlindflem1  37954  poimirlem29  37987  poimirlem32  37990  itg2addnclem3  38011  ftc1cnnc  38030  ftc1anclem6  38036  ftc1anclem7  38037  geomcau  38097  lfli  39524  lfladd  39529  docavalN  41586  diaocN  41588  dihjatc  41880  dvh4dimat  41901  sticksstones10  42611  sticksstones12a  42613  irrapxlem3  43273  irrapxlem4  43274  pellexlem6  43283  rmxfval  43353  rmyfval  43354  hashnzfz  44768  hashnzfzclim  44770  caucvgbf  45938  cvgcaule  45940  climsuse  46059  mullimc  46067  climf  46073  mullimcf  46074  idlimc  46077  limcperiod  46079  clim2f  46085  limcleqr  46093  limclner  46100  climf2  46115  clim2f2  46119  fnlimabslt  46128  climuz  46193  fperdvper  46368  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  stoweidlem9  46458  wallispilem4  46517  wallispilem5  46518  dirkerval  46540  dirkerval2  46543  dirkertrigeqlem1  46547  dirkertrigeqlem2  46548  dirkertrigeq  46550  dirkercncflem2  46553  ovnhoi  47052  hspmbllem1  47075  digfval  49088  dignn0flhalflem2  49107  dfinito4  49991  ranfval  50104