Theorem fvoveq1d 7409

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6511  (class class class)co 7387

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  fvoveq1  7410  imbrov2fvoveq  7412  hashfzp1  14396  pfxfvlsw  14660  swrdswrd  14670  revrev  14732  cshwidx0mod  14770  2cshw  14778  lswcshw  14780  cshweqrep  14786  cshimadifsn0  14796  lswco  14805  cau3lem  15321  clim  15460  rlim  15461  rlim2  15462  clim2  15470  rlimclim  15512  climrlim2  15513  climshftlem  15540  rlimcn3  15556  climcn2  15559  subcn2  15561  isercoll  15634  climcau  15637  caurcvg2  15644  caucvgb  15646  iseralt  15651  climcndslem1  15815  smumullem  16462  prmreclem4  16890  cshwsidrepsw  17064  efgredlem  19677  islmhm2  20945  coe1pwmul  22165  coe1sclmul  22168  evl1gsumadd  22245  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  mpomulcn  24758  mulc1cncf  24798  pcovalg  24912  ehl1eudisval  25321  ovolunlem1a  25397  ovolunlem1  25398  mbfi1fseq  25622  isibl  25666  isibl2  25667  cbvitg  25677  cbvitgv  25678  itgeqa  25715  dveflem  25883  dvferm1lem  25888  dvferm1  25889  dvferm2lem  25890  dvferm2  25891  dvlip  25898  c1lip1  25902  lhop1lem  25918  lhop1  25919  ftc1lem5  25947  vieta1lem2  26219  aalioulem3  26242  ulmshftlem  26298  ulmcaulem  26303  ulmcau  26304  ulmdvlem3  26311  rlimcnp  26875  scvxcvx  26896  jensenlem2  26898  lgamgulmlem2  26940  lgamgulmlem5  26943  lgamgulm2  26946  lgamcvglem  26950  lgamcvg2  26965  basellem4  26994  basellem5  26995  pcbcctr  27187  dchrisumlem3  27402  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumlema  27411  dchrvmasumiflem1  27412  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem2  27429  dchrisum0  27431  chpdifbndlem1  27464  selbergsb  27486  pntlemo  27518  crctcshwlkn0lem2  29741  crctcshwlkn0lem3  29742  crctcshlem4  29750  crctcsh  29754  clwwisshclwwslemlem  29942  lnolin  30683  lnoadd  30687  norm3adifi  31082  lnopl  31843  lnfnl  31860  lnopaddi  31900  lnfnaddi  31972  pfxlsw2ccat  32872  constrrtlc1  33722  constrrtcc  33725  lmatfval  33804  xrge0iifhom  33927  itgeq12dv  34317  signsply0  34542  revwlk  35112  snmlval  35318  iprodgam  35729  cbvitgvw2  36236  cbvitgdavw  36269  cbvitgdavw2  36285  knoppcnlem1  36481  knoppndvlem21  36520  matunitlindflem1  37610  poimirlem29  37643  poimirlem32  37646  itg2addnclem3  37667  ftc1cnnc  37686  ftc1anclem6  37692  ftc1anclem7  37693  geomcau  37753  lfli  39054  lfladd  39059  docavalN  41117  diaocN  41119  dihjatc  41411  dvh4dimat  41432  sticksstones10  42143  sticksstones12a  42145  irrapxlem3  42812  irrapxlem4  42813  pellexlem6  42822  rmxfval  42892  rmyfval  42893  hashnzfz  44309  hashnzfzclim  44311  caucvgbf  45485  cvgcaule  45487  climsuse  45606  mullimc  45614  climf  45620  mullimcf  45621  idlimc  45624  limcperiod  45626  clim2f  45634  limcleqr  45642  limclner  45649  climf2  45664  clim2f2  45668  fnlimabslt  45677  climuz  45742  fperdvper  45917  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  stoweidlem9  46007  wallispilem4  46066  wallispilem5  46067  dirkerval  46089  dirkerval2  46092  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeq  46099  dirkercncflem2  46102  ovnhoi  46601  hspmbllem1  46624  digfval  48586  dignn0flhalflem2  48605  dfinito4  49490  ranfval  49603