Theorem fvoveq1d 7389

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6498  (class class class)co 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  fvoveq1  7390  imbrov2fvoveq  7392  hashfzp1  14393  pfxfvlsw  14657  swrdswrd  14667  revrev  14729  cshwidx0mod  14767  2cshw  14775  lswcshw  14777  cshweqrep  14783  cshimadifsn0  14792  lswco  14801  cau3lem  15317  clim  15456  rlim  15457  rlim2  15458  clim2  15466  rlimclim  15508  climrlim2  15509  climshftlem  15536  rlimcn3  15552  climcn2  15555  subcn2  15557  isercoll  15630  climcau  15633  caurcvg2  15640  caucvgb  15642  iseralt  15647  climcndslem1  15814  smumullem  16461  prmreclem4  16890  cshwsidrepsw  17064  efgredlem  19722  islmhm2  21033  coe1pwmul  22244  coe1sclmul  22247  evl1gsumadd  22323  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  mpomulcn  24834  mulc1cncf  24872  pcovalg  24979  ehl1eudisval  25388  ovolunlem1a  25463  ovolunlem1  25464  mbfi1fseq  25688  isibl  25732  isibl2  25733  cbvitg  25743  cbvitgv  25744  itgeqa  25781  dveflem  25946  dvferm1lem  25951  dvferm1  25952  dvferm2lem  25953  dvferm2  25954  dvlip  25960  c1lip1  25964  lhop1lem  25980  lhop1  25981  ftc1lem5  26007  vieta1lem2  26277  aalioulem3  26300  ulmshftlem  26354  ulmcaulem  26359  ulmcau  26360  ulmdvlem3  26367  rlimcnp  26929  scvxcvx  26949  jensenlem2  26951  lgamgulmlem2  26993  lgamgulmlem5  26996  lgamgulm2  26999  lgamcvglem  27003  lgamcvg2  27018  basellem4  27047  basellem5  27048  pcbcctr  27239  dchrisumlem3  27454  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumlema  27463  dchrvmasumiflem1  27464  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem2  27481  dchrisum0  27483  chpdifbndlem1  27516  selbergsb  27538  pntlemo  27570  crctcshwlkn0lem2  29879  crctcshwlkn0lem3  29880  crctcshlem4  29888  crctcsh  29892  clwwisshclwwslemlem  30083  lnolin  30825  lnoadd  30829  norm3adifi  31224  lnopl  31985  lnfnl  32002  lnopaddi  32042  lnfnaddi  32114  pfxlsw2ccat  33010  extvfval  33676  mplvrpmrhm  33691  constrrtlc1  33876  constrrtcc  33879  lmatfval  33958  xrge0iifhom  34081  itgeq12dv  34470  signsply0  34695  revwlk  35307  snmlval  35513  iprodgam  35924  cbvitgvw2  36430  cbvitgdavw  36463  cbvitgdavw2  36479  knoppcnlem1  36753  knoppndvlem21  36792  matunitlindflem1  37937  poimirlem29  37970  poimirlem32  37973  itg2addnclem3  37994  ftc1cnnc  38013  ftc1anclem6  38019  ftc1anclem7  38020  geomcau  38080  lfli  39507  lfladd  39512  docavalN  41569  diaocN  41571  dihjatc  41863  dvh4dimat  41884  sticksstones10  42594  sticksstones12a  42596  irrapxlem3  43252  irrapxlem4  43253  pellexlem6  43262  rmxfval  43332  rmyfval  43333  hashnzfz  44747  hashnzfzclim  44749  caucvgbf  45917  cvgcaule  45919  climsuse  46038  mullimc  46046  climf  46052  mullimcf  46053  idlimc  46056  limcperiod  46058  clim2f  46064  limcleqr  46072  limclner  46079  climf2  46094  clim2f2  46098  fnlimabslt  46107  climuz  46172  fperdvper  46347  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  stoweidlem9  46437  wallispilem4  46496  wallispilem5  46497  dirkerval  46519  dirkerval2  46522  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeq  46529  dirkercncflem2  46532  ovnhoi  47031  hspmbllem1  47054  digfval  49073  dignn0flhalflem2  49092  dfinito4  49976  ranfval  50089