Theorem fvoveq1d 7425

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6530  (class class class)co 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  fvoveq1  7426  imbrov2fvoveq  7428  hashfzp1  14447  pfxfvlsw  14711  swrdswrd  14721  revrev  14783  cshwidx0mod  14821  2cshw  14829  lswcshw  14831  cshweqrep  14837  cshimadifsn0  14847  lswco  14856  cau3lem  15371  clim  15508  rlim  15509  rlim2  15510  clim2  15518  rlimclim  15560  climrlim2  15561  climshftlem  15588  rlimcn3  15604  climcn2  15607  subcn2  15609  isercoll  15682  climcau  15685  caurcvg2  15692  caucvgb  15694  iseralt  15699  climcndslem1  15863  smumullem  16509  prmreclem4  16937  cshwsidrepsw  17111  efgredlem  19726  islmhm2  20994  coe1pwmul  22214  coe1sclmul  22217  evl1gsumadd  22294  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  mpomulcn  24807  mulc1cncf  24847  pcovalg  24961  ehl1eudisval  25371  ovolunlem1a  25447  ovolunlem1  25448  mbfi1fseq  25672  isibl  25716  isibl2  25717  cbvitg  25727  cbvitgv  25728  itgeqa  25765  dveflem  25933  dvferm1lem  25938  dvferm1  25939  dvferm2lem  25940  dvferm2  25941  dvlip  25948  c1lip1  25952  lhop1lem  25968  lhop1  25969  ftc1lem5  25997  vieta1lem2  26269  aalioulem3  26292  ulmshftlem  26348  ulmcaulem  26353  ulmcau  26354  ulmdvlem3  26361  rlimcnp  26925  scvxcvx  26946  jensenlem2  26948  lgamgulmlem2  26990  lgamgulmlem5  26993  lgamgulm2  26996  lgamcvglem  27000  lgamcvg2  27015  basellem4  27044  basellem5  27045  pcbcctr  27237  dchrisumlem3  27452  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlema  27461  dchrvmasumiflem1  27462  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem2  27479  dchrisum0  27481  chpdifbndlem1  27514  selbergsb  27536  pntlemo  27568  crctcshwlkn0lem2  29739  crctcshwlkn0lem3  29740  crctcshlem4  29748  crctcsh  29752  clwwisshclwwslemlem  29940  lnolin  30681  lnoadd  30685  norm3adifi  31080  lnopl  31841  lnfnl  31858  lnopaddi  31898  lnfnaddi  31970  pfxlsw2ccat  32872  constrrtlc1  33712  constrrtcc  33715  lmatfval  33791  xrge0iifhom  33914  itgeq12dv  34304  signsply0  34529  revwlk  35093  snmlval  35299  iprodgam  35705  cbvitgvw2  36212  cbvitgdavw  36245  cbvitgdavw2  36261  knoppcnlem1  36457  knoppndvlem21  36496  matunitlindflem1  37586  poimirlem29  37619  poimirlem32  37622  itg2addnclem3  37643  ftc1cnnc  37662  ftc1anclem6  37668  ftc1anclem7  37669  geomcau  37729  lfli  39025  lfladd  39030  docavalN  41088  diaocN  41090  dihjatc  41382  dvh4dimat  41403  sticksstones10  42114  sticksstones12a  42116  irrapxlem3  42794  irrapxlem4  42795  pellexlem6  42804  rmxfval  42874  rmyfval  42875  hashnzfz  44292  hashnzfzclim  44294  caucvgbf  45464  cvgcaule  45466  climsuse  45585  mullimc  45593  climf  45599  mullimcf  45600  idlimc  45603  limcperiod  45605  clim2f  45613  limcleqr  45621  limclner  45628  climf2  45643  clim2f2  45647  fnlimabslt  45656  climuz  45721  fperdvper  45896  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmul  45920  stoweidlem9  45986  wallispilem4  46045  wallispilem5  46046  dirkerval  46068  dirkerval2  46071  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeq  46078  dirkercncflem2  46081  ovnhoi  46580  hspmbllem1  46603  digfval  48525  dignn0flhalflem2  48544  dfinito4  49334  ranfval  49439