Theorem fvoveq1d 7306

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

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6437  (class class class)co 7284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  fvoveq1  7307  imbrov2fvoveq  7309  hashfzp1  14155  pfxfvlsw  14417  swrdswrd  14427  revrev  14489  cshwidx0mod  14527  2cshw  14535  lswcshw  14537  cshweqrep  14543  cshimadifsn0  14552  lswco  14561  cau3lem  15075  clim  15212  rlim  15213  rlim2  15214  clim2  15222  rlimclim  15264  climrlim2  15265  climshftlem  15292  rlimcn3  15308  climcn2  15311  subcn2  15313  isercoll  15388  climcau  15391  caurcvg2  15398  caucvgb  15400  iseralt  15405  climcndslem1  15570  smumullem  16208  prmreclem4  16629  cshwsidrepsw  16804  efgredlem  19362  islmhm2  20309  coe1pwmul  21459  coe1sclmul  21462  evl1gsumadd  21533  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  mulc1cncf  24077  pcovalg  24184  ehl1eudisval  24594  ovolunlem1a  24669  ovolunlem1  24670  mbfi1fseq  24895  isibl  24939  isibl2  24940  cbvitg  24949  itgeqa  24987  dveflem  25152  dvferm1lem  25157  dvferm1  25158  dvferm2lem  25159  dvferm2  25160  dvlip  25166  c1lip1  25170  lhop1lem  25186  lhop1  25187  ftc1lem5  25213  vieta1lem2  25480  aalioulem3  25503  ulmshftlem  25557  ulmcaulem  25562  ulmcau  25563  ulmdvlem3  25570  rlimcnp  26124  scvxcvx  26144  jensenlem2  26146  lgamgulmlem2  26188  lgamgulmlem5  26191  lgamgulm2  26194  lgamcvglem  26198  lgamcvg2  26213  basellem4  26242  basellem5  26243  pcbcctr  26433  dchrisumlem3  26648  dchrmusumlema  26650  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlema  26657  dchrvmasumiflem1  26658  dchrisum0lema  26671  dchrisum0lem1b  26672  dchrisum0lem2  26675  dchrisum0  26677  chpdifbndlem1  26710  selbergsb  26732  pntlemo  26764  crctcshwlkn0lem2  28185  crctcshwlkn0lem3  28186  crctcshlem4  28194  crctcsh  28198  clwwisshclwwslemlem  28386  lnolin  29125  lnoadd  29129  norm3adifi  29524  lnopl  30285  lnfnl  30302  lnopaddi  30342  lnfnaddi  30414  pfxlsw2ccat  31233  lmatfval  31773  xrge0iifhom  31896  itgeq12dv  32302  signsply0  32539  revwlk  33095  snmlval  33302  iprodgam  33717  knoppcnlem1  34682  knoppndvlem21  34721  matunitlindflem1  35782  poimirlem29  35815  poimirlem32  35818  itg2addnclem3  35839  ftc1cnnc  35858  ftc1anclem6  35864  ftc1anclem7  35865  geomcau  35926  lfli  37082  lfladd  37087  docavalN  39144  diaocN  39146  dihjatc  39438  dvh4dimat  39459  sticksstones10  40118  sticksstones12a  40120  irrapxlem3  40653  irrapxlem4  40654  pellexlem6  40663  rmxfval  40733  rmyfval  40734  hashnzfz  41945  hashnzfzclim  41947  climsuse  43156  mullimc  43164  climf  43170  mullimcf  43171  idlimc  43174  limcperiod  43176  clim2f  43184  limcleqr  43192  limclner  43199  climf2  43214  clim2f2  43218  fnlimabslt  43227  climuz  43292  fperdvper  43467  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  stoweidlem9  43557  wallispilem4  43616  wallispilem5  43617  dirkerval  43639  dirkerval2  43642  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeq  43649  dirkercncflem2  43652  ovnhoi  44148  hspmbllem1  44171  digfval  45954  dignn0flhalflem2  45973