Theorem fvoveq1d 7368

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6481  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  fvoveq1  7369  imbrov2fvoveq  7371  hashfzp1  14338  pfxfvlsw  14602  swrdswrd  14612  revrev  14674  cshwidx0mod  14712  2cshw  14720  lswcshw  14722  cshweqrep  14728  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  19659  islmhm2  20972  coe1pwmul  22193  coe1sclmul  22196  evl1gsumadd  22273  chfacfscmulgsum  22775  chfacfpmmulgsum  22779  mpomulcn  24785  mulc1cncf  24825  pcovalg  24939  ehl1eudisval  25348  ovolunlem1a  25424  ovolunlem1  25425  mbfi1fseq  25649  isibl  25693  isibl2  25694  cbvitg  25704  cbvitgv  25705  itgeqa  25742  dveflem  25910  dvferm1lem  25915  dvferm1  25916  dvferm2lem  25917  dvferm2  25918  dvlip  25925  c1lip1  25929  lhop1lem  25945  lhop1  25946  ftc1lem5  25974  vieta1lem2  26246  aalioulem3  26269  ulmshftlem  26325  ulmcaulem  26330  ulmcau  26331  ulmdvlem3  26338  rlimcnp  26902  scvxcvx  26923  jensenlem2  26925  lgamgulmlem2  26967  lgamgulmlem5  26970  lgamgulm2  26973  lgamcvglem  26977  lgamcvg2  26992  basellem4  27021  basellem5  27022  pcbcctr  27214  dchrisumlem3  27429  dchrmusumlema  27431  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumlema  27438  dchrvmasumiflem1  27439  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem2  27456  dchrisum0  27458  chpdifbndlem1  27491  selbergsb  27513  pntlemo  27545  crctcshwlkn0lem2  29789  crctcshwlkn0lem3  29790  crctcshlem4  29798  crctcsh  29802  clwwisshclwwslemlem  29993  lnolin  30734  lnoadd  30738  norm3adifi  31133  lnopl  31894  lnfnl  31911  lnopaddi  31951  lnfnaddi  32023  pfxlsw2ccat  32931  mplvrpmrhm  33577  constrrtlc1  33745  constrrtcc  33748  lmatfval  33827  xrge0iifhom  33950  itgeq12dv  34339  signsply0  34564  revwlk  35169  snmlval  35375  iprodgam  35786  cbvitgvw2  36292  cbvitgdavw  36325  cbvitgdavw2  36341  knoppcnlem1  36537  knoppndvlem21  36576  matunitlindflem1  37666  poimirlem29  37699  poimirlem32  37702  itg2addnclem3  37723  ftc1cnnc  37742  ftc1anclem6  37748  ftc1anclem7  37749  geomcau  37809  lfli  39170  lfladd  39175  docavalN  41232  diaocN  41234  dihjatc  41526  dvh4dimat  41547  sticksstones10  42258  sticksstones12a  42260  irrapxlem3  42927  irrapxlem4  42928  pellexlem6  42937  rmxfval  43007  rmyfval  43008  hashnzfz  44423  hashnzfzclim  44425  caucvgbf  45597  cvgcaule  45599  climsuse  45718  mullimc  45726  climf  45732  mullimcf  45733  idlimc  45736  limcperiod  45738  clim2f  45744  limcleqr  45752  limclner  45759  climf2  45774  clim2f2  45778  fnlimabslt  45787  climuz  45852  fperdvper  46027  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnmul  46051  stoweidlem9  46117  wallispilem4  46176  wallispilem5  46177  dirkerval  46199  dirkerval2  46202  dirkertrigeqlem1  46206  dirkertrigeqlem2  46207  dirkertrigeq  46209  dirkercncflem2  46212  ovnhoi  46711  hspmbllem1  46734  digfval  48708  dignn0flhalflem2  48727  dfinito4  49612  ranfval  49725