Theorem fvoveq1d 7380

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6490  (class class class)co 7358

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 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  fvoveq1  7381  imbrov2fvoveq  7383  hashfzp1  14382  pfxfvlsw  14646  swrdswrd  14656  revrev  14718  cshwidx0mod  14756  2cshw  14764  lswcshw  14766  cshweqrep  14772  cshimadifsn0  14781  lswco  14790  cau3lem  15306  clim  15445  rlim  15446  rlim2  15447  clim2  15455  rlimclim  15497  climrlim2  15498  climshftlem  15525  rlimcn3  15541  climcn2  15544  subcn2  15546  isercoll  15619  climcau  15622  caurcvg2  15629  caucvgb  15631  iseralt  15636  climcndslem1  15803  smumullem  16450  prmreclem4  16879  cshwsidrepsw  17053  efgredlem  19711  islmhm2  21023  coe1pwmul  22253  coe1sclmul  22256  evl1gsumadd  22332  chfacfscmulgsum  22834  chfacfpmmulgsum  22838  mpomulcn  24843  mulc1cncf  24881  pcovalg  24988  ehl1eudisval  25397  ovolunlem1a  25472  ovolunlem1  25473  mbfi1fseq  25697  isibl  25741  isibl2  25742  cbvitg  25752  cbvitgv  25753  itgeqa  25790  dveflem  25955  dvferm1lem  25960  dvferm1  25961  dvferm2lem  25962  dvferm2  25963  dvlip  25970  c1lip1  25974  lhop1lem  25990  lhop1  25991  ftc1lem5  26019  vieta1lem2  26290  aalioulem3  26313  ulmshftlem  26369  ulmcaulem  26374  ulmcau  26375  ulmdvlem3  26382  rlimcnp  26946  scvxcvx  26967  jensenlem2  26969  lgamgulmlem2  27011  lgamgulmlem5  27014  lgamgulm2  27017  lgamcvglem  27021  lgamcvg2  27036  basellem4  27065  basellem5  27066  pcbcctr  27258  dchrisumlem3  27473  dchrmusumlema  27475  dchrmusum2  27476  dchrvmasumlem2  27480  dchrvmasumlema  27482  dchrvmasumiflem1  27483  dchrisum0lema  27496  dchrisum0lem1b  27497  dchrisum0lem2  27500  dchrisum0  27502  chpdifbndlem1  27535  selbergsb  27557  pntlemo  27589  crctcshwlkn0lem2  29899  crctcshwlkn0lem3  29900  crctcshlem4  29908  crctcsh  29912  clwwisshclwwslemlem  30103  lnolin  30845  lnoadd  30849  norm3adifi  31244  lnopl  32005  lnfnl  32022  lnopaddi  32062  lnfnaddi  32134  pfxlsw2ccat  33030  extvfval  33696  mplvrpmrhm  33711  constrrtlc1  33897  constrrtcc  33900  lmatfval  33979  xrge0iifhom  34102  itgeq12dv  34491  signsply0  34716  revwlk  35328  snmlval  35534  iprodgam  35945  cbvitgvw2  36451  cbvitgdavw  36484  cbvitgdavw2  36500  knoppcnlem1  36766  knoppndvlem21  36805  matunitlindflem1  37948  poimirlem29  37981  poimirlem32  37984  itg2addnclem3  38005  ftc1cnnc  38024  ftc1anclem6  38030  ftc1anclem7  38031  geomcau  38091  lfli  39518  lfladd  39523  docavalN  41580  diaocN  41582  dihjatc  41874  dvh4dimat  41895  sticksstones10  42605  sticksstones12a  42607  irrapxlem3  43267  irrapxlem4  43268  pellexlem6  43277  rmxfval  43347  rmyfval  43348  hashnzfz  44762  hashnzfzclim  44764  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  49070  dignn0flhalflem2  49089  dfinito4  49973  ranfval  50086