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 6831	1 ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1547  ‘cfv 6485  (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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  fvoveq1  7379  imbrov2fvoveq  7381  hashfzp1  14384  pfxfvlsw  14648  swrdswrd  14658  revrev  14720  cshwidx0mod  14758  2cshw  14766  lswcshw  14768  cshweqrep  14774  cshimadifsn0  14783  lswco  14792  cau3lem  15308  clim  15447  rlim  15448  rlim2  15449  clim2  15457  rlimclim  15499  climrlim2  15500  climshftlem  15527  rlimcn3  15543  climcn2  15546  subcn2  15548  isercoll  15621  climcau  15624  caurcvg2  15631  caucvgb  15633  iseralt  15638  climcndslem1  15805  smumullem  16452  prmreclem4  16881  cshwsidrepsw  17055  efgredlem  19713  islmhm2  21028  coe1pwmul  22265  coe1sclmul  22268  evl1gsumadd  22344  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  mpomulcn  24852  mulc1cncf  24890  pcovalg  24997  ehl1eudisval  25406  ovolunlem1a  25481  ovolunlem1  25482  mbfi1fseq  25706  isibl  25750  isibl2  25751  cbvitg  25761  cbvitgv  25762  itgeqa  25799  dveflem  25964  dvferm1lem  25969  dvferm1  25970  dvferm2lem  25971  dvferm2  25972  dvlip  25978  c1lip1  25982  lhop1lem  25998  lhop1  25999  ftc1lem5  26025  vieta1lem2  26295  aalioulem3  26318  ulmshftlem  26372  ulmcaulem  26377  ulmcau  26378  ulmdvlem3  26385  rlimcnp  26947  scvxcvx  26967  jensenlem2  26969  lgamgulmlem2  27011  lgamgulmlem5  27014  lgamgulm2  27017  lgamcvglem  27021  lgamcvg2  27036  basellem4  27065  basellem5  27066  pcbcctr  27257  dchrisumlem3  27472  dchrmusumlema  27474  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumlema  27481  dchrvmasumiflem1  27482  dchrisum0lema  27495  dchrisum0lem1b  27496  dchrisum0lem2  27499  dchrisum0  27501  chpdifbndlem1  27534  selbergsb  27556  pntlemo  27588  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  33029  extvfval  33716  mplvrpmrhm  33731  constrrtlc1  33916  constrrtcc  33919  lmatfval  33998  xrge0iifhom  34121  itgeq12dv  34510  signsply0  34735  revwlk  35353  snmlval  35559  iprodgam  35970  cbvitgvw2  36476  cbvitgdavw  36509  cbvitgdavw2  36525  knoppcnlem1  36799  knoppndvlem21  36838  matunitlindflem1  37983  poimirlem29  38016  poimirlem32  38019  itg2addnclem3  38040  ftc1cnnc  38059  ftc1anclem6  38065  ftc1anclem7  38066  geomcau  38126  lfli  39553  lfladd  39558  docavalN  41615  diaocN  41617  dihjatc  41909  dvh4dimat  41930  sticksstones10  42640  sticksstones12a  42642  irrapxlem3  43269  irrapxlem4  43270  pellexlem6  43279  rmxfval  43349  rmyfval  43350  hashnzfz  44764  hashnzfzclim  44766  caucvgbf  45932  cvgcaule  45934  climsuse  46053  mullimc  46061  climf  46067  mullimcf  46068  idlimc  46071  limcperiod  46073  clim2f  46079  limcleqr  46087  limclner  46094  climf2  46109  clim2f2  46113  fnlimabslt  46122  climuz  46187  fperdvper  46362  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnmul  46386  stoweidlem9  46452  wallispilem4  46511  wallispilem5  46512  dirkerval  46534  dirkerval2  46537  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeq  46544  dirkercncflem2  46547  ovnhoi  47046  hspmbllem1  47069  digfval  49088  dignn0flhalflem2  49107  dfinito4  49991  ranfval  50104