Theorem fvoveq1d 7178

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

Syntax hints:   → wi 4   = wceq 1537  ‘cfv 6355  (class class class)co 7156

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  fvoveq1  7179  imbrov2fvoveq  7181  hashfzp1  13793  pfxfvlsw  14057  swrdswrd  14067  revrev  14129  cshwidx0mod  14167  2cshw  14175  lswcshw  14177  cshweqrep  14183  cshimadifsn0  14192  lswco  14201  cau3lem  14714  clim  14851  rlim  14852  rlim2  14853  clim2  14861  rlimclim  14903  climrlim2  14904  climshftlem  14931  rlimcn2  14947  climcn2  14949  subcn2  14951  isercoll  15024  climcau  15027  caurcvg2  15034  caucvgb  15036  iseralt  15041  climcndslem1  15204  smumullem  15841  prmreclem4  16255  cshwsidrepsw  16427  efgredlem  18873  islmhm2  19810  coe1pwmul  20447  coe1sclmul  20450  evl1gsumadd  20521  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  mulc1cncf  23513  pcovalg  23616  ehl1eudisval  24024  ovolunlem1a  24097  ovolunlem1  24098  mbfi1fseq  24322  isibl  24366  isibl2  24367  cbvitg  24376  itgeqa  24414  dveflem  24576  dvferm1lem  24581  dvferm1  24582  dvferm2lem  24583  dvferm2  24584  dvlip  24590  c1lip1  24594  lhop1lem  24610  lhop1  24611  ftc1lem5  24637  vieta1lem2  24900  aalioulem3  24923  ulmshftlem  24977  ulmcaulem  24982  ulmcau  24983  ulmdvlem3  24990  rlimcnp  25543  scvxcvx  25563  jensenlem2  25565  lgamgulmlem2  25607  lgamgulmlem5  25610  lgamgulm2  25613  lgamcvglem  25617  lgamcvg2  25632  basellem4  25661  basellem5  25662  pcbcctr  25852  dchrisumlem3  26067  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem2  26094  dchrisum0  26096  chpdifbndlem1  26129  selbergsb  26151  pntlemo  26183  crctcshwlkn0lem2  27589  crctcshwlkn0lem3  27590  crctcshlem4  27598  crctcsh  27602  clwwisshclwwslemlem  27791  lnolin  28531  lnoadd  28535  norm3adifi  28930  lnopl  29691  lnfnl  29708  lnopaddi  29748  lnfnaddi  29820  pfxlsw2ccat  30626  lmatfval  31079  xrge0iifhom  31180  itgeq12dv  31584  signsply0  31821  revwlk  32371  snmlval  32578  iprodgam  32974  knoppcnlem1  33832  knoppndvlem21  33871  matunitlindflem1  34903  poimirlem29  34936  poimirlem32  34939  itg2addnclem3  34960  ftc1cnnc  34981  ftc1anclem6  34987  ftc1anclem7  34988  geomcau  35049  lfli  36212  lfladd  36217  docavalN  38274  diaocN  38276  dihjatc  38568  dvh4dimat  38589  irrapxlem3  39441  irrapxlem4  39442  pellexlem6  39451  rmxfval  39521  rmyfval  39522  hashnzfz  40672  hashnzfzclim  40674  climsuse  41909  mullimc  41917  climf  41923  mullimcf  41924  idlimc  41927  limcperiod  41929  clim2f  41937  limcleqr  41945  limclner  41952  climf2  41967  clim2f2  41971  fnlimabslt  41980  climuz  42045  fperdvper  42223  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnmul  42248  stoweidlem9  42314  wallispilem4  42373  wallispilem5  42374  dirkerval  42396  dirkerval2  42399  dirkertrigeqlem1  42403  dirkertrigeqlem2  42404  dirkertrigeq  42406  dirkercncflem2  42409  ovnhoi  42905  hspmbllem1  42928  digfval  44677  dignn0flhalflem2  44696