Theorem fvoveq1d 7439

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6537  (class class class)co 7417

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420

This theorem is used by:  fvoveq1  7440  imbrov2fvoveq  7442  hashfzp1  14500  pfxfvlsw  14768  swrdswrd  14778  revrev  14840  cshwidx0mod  14880  2cshw  14888  lswcshw  14890  cshweqrep  14896  cshimadifsn0  14905  lswco  14914  cau3lem  15446  clim  15585  rlim  15586  rlim2  15587  clim2  15595  rlimclim  15637  climrlim2  15638  climshftlem  15665  rlimcn3  15681  climcn2  15684  subcn2  15686  isercoll  15759  climcau  15762  caurcvg2  15769  caucvgb  15771  iseralt  15776  climcndslem1  15942  smumullem  16588  prmreclem4  17017  cshwsidrepsw  17191  efgredlem  19880  islmhm2  21228  coe1pwmul  22511  coe1sclmul  22514  evl1gsumadd  22589  matunitlindflem1  22907  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  mpomulcn  25101  mulc1cncf  25139  pcovalg  25246  ehl1eudisval  25655  ovolunlem1a  25730  ovolunlem1  25731  mbfi1fseq  25955  isibl  25999  isibl2  26000  cbvitg  26010  cbvitgv  26011  itgeqa  26048  dveflem  26213  dvferm1lem  26218  dvferm1  26219  dvferm2lem  26220  dvferm2  26221  dvlip  26227  c1lip1  26231  lhop1lem  26247  lhop1  26248  ftc1lem5  26274  vieta1lem2  26550  aalioulem3  26577  ulmshftlem  26632  ulmcaulem  26637  ulmcau  26638  ulmdvlem3  26645  rlimcnp  27210  scvxcvx  27230  jensenlem2  27232  lgamgulmlem2  27274  lgamgulmlem5  27277  lgamgulm2  27280  lgamcvglem  27284  lgamcvg2  27299  basellem4  27328  basellem5  27329  pcbcctr  27520  dchrisumlem3  27735  dchrmusumlema  27737  dchrmusum2  27738  dchrvmasumlem2  27742  dchrvmasumlema  27744  dchrvmasumiflem1  27745  dchrisum0lema  27758  dchrisum0lem1b  27759  dchrisum0lem2  27762  dchrisum0  27764  chpdifbndlem1  27797  selbergsb  27819  pntlemo  27851  revwlk  30154  crctcshwlkn0lem2  30287  crctcshwlkn0lem3  30288  crctcshlem4  30296  crctcsh  30300  clwwisshclwwslemlem  30491  lnolin  31243  lnoadd  31247  norm3adifi  31642  lnopl  32403  lnfnl  32420  lnopaddi  32460  lnfnaddi  32532  pfxlsw2ccat  33400  extvfval  34050  mplvrpmrhm  34065  constrrtlc1  34250  constrrtcc  34253  lmatfval  34332  xrge0iifhom  34455  itgeq12dv  34845  signsply0  35067  snmlval  35918  iprodgam  36329  cbvitgvw2  36876  cbvitgdavw  36909  cbvitgdavw2  36925  knoppcnlem1  37198  knoppndvlem21  37237  poimirlem29  38406  poimirlem32  38409  itg2addnclem3  38430  ftc1cnnc  38449  ftc1anclem6  38455  ftc1anclem7  38456  geomcau  38517  lfli  39942  lfladd  39947  docavalN  42004  diaocN  42006  dihjatc  42298  dvh4dimat  42319  sticksstones10  43029  sticksstones12a  43031  irrapxlem3  43673  irrapxlem4  43674  pellexlem6  43683  rmxfval  43753  rmyfval  43754  hashnzfz  45152  hashnzfzclim  45154  caucvgbf  46325  cvgcaule  46327  climsuse  46446  mullimc  46454  climf  46460  mullimcf  46461  idlimc  46464  limcperiod  46466  clim2f  46472  limcleqr  46480  limclner  46487  climf2  46502  clim2f2  46506  fnlimabslt  46515  climuz  46580  fperdvper  46755  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnmul  46779  stoweidlem9  46845  wallispilem4  46904  wallispilem5  46905  dirkerval  46927  dirkerval2  46930  dirkertrigeqlem1  46934  dirkertrigeqlem2  46935  dirkertrigeq  46937  dirkercncflem2  46940  fourierdlem48  46990  fourierdlem49  46991  fourierdlem113  47055  ovnhoi  47439  hspmbllem1  47462  digfval  49535  dignn0flhalflem2  49554  dfinito4  50435  ranfval  50548