Theorem fvoveq1d 7452

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

Syntax hints:   → wi 4   = wceq 1536  ‘cfv 6562  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  fvoveq1  7453  imbrov2fvoveq  7455  hashfzp1  14466  pfxfvlsw  14729  swrdswrd  14739  revrev  14801  cshwidx0mod  14839  2cshw  14847  lswcshw  14849  cshweqrep  14855  cshimadifsn0  14865  lswco  14874  cau3lem  15389  clim  15526  rlim  15527  rlim2  15528  clim2  15536  rlimclim  15578  climrlim2  15579  climshftlem  15606  rlimcn3  15622  climcn2  15625  subcn2  15627  isercoll  15700  climcau  15703  caurcvg2  15710  caucvgb  15712  iseralt  15717  climcndslem1  15881  smumullem  16525  prmreclem4  16952  cshwsidrepsw  17127  efgredlem  19779  islmhm2  21054  coe1pwmul  22297  coe1sclmul  22300  evl1gsumadd  22377  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  mpomulcn  24904  mulc1cncf  24944  pcovalg  25058  ehl1eudisval  25468  ovolunlem1a  25544  ovolunlem1  25545  mbfi1fseq  25770  isibl  25814  isibl2  25815  cbvitg  25825  cbvitgv  25826  itgeqa  25863  dveflem  26031  dvferm1lem  26036  dvferm1  26037  dvferm2lem  26038  dvferm2  26039  dvlip  26046  c1lip1  26050  lhop1lem  26066  lhop1  26067  ftc1lem5  26095  vieta1lem2  26367  aalioulem3  26390  ulmshftlem  26446  ulmcaulem  26451  ulmcau  26452  ulmdvlem3  26459  rlimcnp  27022  scvxcvx  27043  jensenlem2  27045  lgamgulmlem2  27087  lgamgulmlem5  27090  lgamgulm2  27093  lgamcvglem  27097  lgamcvg2  27112  basellem4  27141  basellem5  27142  pcbcctr  27334  dchrisumlem3  27549  dchrmusumlema  27551  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumlema  27558  dchrvmasumiflem1  27559  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem2  27576  dchrisum0  27578  chpdifbndlem1  27611  selbergsb  27633  pntlemo  27665  crctcshwlkn0lem2  29840  crctcshwlkn0lem3  29841  crctcshlem4  29849  crctcsh  29853  clwwisshclwwslemlem  30041  lnolin  30782  lnoadd  30786  norm3adifi  31181  lnopl  31942  lnfnl  31959  lnopaddi  31999  lnfnaddi  32071  pfxlsw2ccat  32919  constrrtlc1  33737  constrrtcc  33740  lmatfval  33774  xrge0iifhom  33897  itgeq12dv  34307  signsply0  34544  revwlk  35108  snmlval  35315  iprodgam  35721  cbvitgvw2  36230  cbvitgdavw  36263  cbvitgdavw2  36279  knoppcnlem1  36475  knoppndvlem21  36514  matunitlindflem1  37602  poimirlem29  37635  poimirlem32  37638  itg2addnclem3  37659  ftc1cnnc  37678  ftc1anclem6  37684  ftc1anclem7  37685  geomcau  37745  lfli  39042  lfladd  39047  docavalN  41105  diaocN  41107  dihjatc  41399  dvh4dimat  41420  sticksstones10  42136  sticksstones12a  42138  irrapxlem3  42811  irrapxlem4  42812  pellexlem6  42821  rmxfval  42891  rmyfval  42892  hashnzfz  44315  hashnzfzclim  44317  caucvgbf  45439  cvgcaule  45441  climsuse  45563  mullimc  45571  climf  45577  mullimcf  45578  idlimc  45581  limcperiod  45583  clim2f  45591  limcleqr  45599  limclner  45606  climf2  45621  clim2f2  45625  fnlimabslt  45634  climuz  45699  fperdvper  45874  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmul  45898  stoweidlem9  45964  wallispilem4  46023  wallispilem5  46024  dirkerval  46046  dirkerval2  46049  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeq  46056  dirkercncflem2  46059  ovnhoi  46558  hspmbllem1  46581  digfval  48446  dignn0flhalflem2  48465