Theorem fvoveq1d 7433

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

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6542  (class class class)co 7411

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414

This theorem is referenced by:  fvoveq1  7434  imbrov2fvoveq  7436  hashfzp1  14395  pfxfvlsw  14649  swrdswrd  14659  revrev  14721  cshwidx0mod  14759  2cshw  14767  lswcshw  14769  cshweqrep  14775  cshimadifsn0  14785  lswco  14794  cau3lem  15305  clim  15442  rlim  15443  rlim2  15444  clim2  15452  rlimclim  15494  climrlim2  15495  climshftlem  15522  rlimcn3  15538  climcn2  15541  subcn2  15543  isercoll  15618  climcau  15621  caurcvg2  15628  caucvgb  15630  iseralt  15635  climcndslem1  15799  smumullem  16437  prmreclem4  16856  cshwsidrepsw  17031  efgredlem  19656  islmhm2  20793  coe1pwmul  22021  coe1sclmul  22024  evl1gsumadd  22097  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  mpomulcn  24605  mulc1cncf  24645  pcovalg  24759  ehl1eudisval  25169  ovolunlem1a  25245  ovolunlem1  25246  mbfi1fseq  25471  isibl  25515  isibl2  25516  cbvitg  25525  itgeqa  25563  dveflem  25731  dvferm1lem  25736  dvferm1  25737  dvferm2lem  25738  dvferm2  25739  dvlip  25745  c1lip1  25749  lhop1lem  25765  lhop1  25766  ftc1lem5  25792  vieta1lem2  26060  aalioulem3  26083  ulmshftlem  26137  ulmcaulem  26142  ulmcau  26143  ulmdvlem3  26150  rlimcnp  26706  scvxcvx  26726  jensenlem2  26728  lgamgulmlem2  26770  lgamgulmlem5  26773  lgamgulm2  26776  lgamcvglem  26780  lgamcvg2  26795  basellem4  26824  basellem5  26825  pcbcctr  27015  dchrisumlem3  27230  dchrmusumlema  27232  dchrmusum2  27233  dchrvmasumlem2  27237  dchrvmasumlema  27239  dchrvmasumiflem1  27240  dchrisum0lema  27253  dchrisum0lem1b  27254  dchrisum0lem2  27257  dchrisum0  27259  chpdifbndlem1  27292  selbergsb  27314  pntlemo  27346  crctcshwlkn0lem2  29332  crctcshwlkn0lem3  29333  crctcshlem4  29341  crctcsh  29345  clwwisshclwwslemlem  29533  lnolin  30274  lnoadd  30278  norm3adifi  30673  lnopl  31434  lnfnl  31451  lnopaddi  31491  lnfnaddi  31563  pfxlsw2ccat  32383  lmatfval  33092  xrge0iifhom  33215  itgeq12dv  33623  signsply0  33860  revwlk  34413  snmlval  34620  iprodgam  35016  knoppcnlem1  35672  knoppndvlem21  35711  matunitlindflem1  36787  poimirlem29  36820  poimirlem32  36823  itg2addnclem3  36844  ftc1cnnc  36863  ftc1anclem6  36869  ftc1anclem7  36870  geomcau  36930  lfli  38234  lfladd  38239  docavalN  40297  diaocN  40299  dihjatc  40591  dvh4dimat  40612  sticksstones10  41277  sticksstones12a  41279  irrapxlem3  41864  irrapxlem4  41865  pellexlem6  41874  rmxfval  41944  rmyfval  41945  hashnzfz  43381  hashnzfzclim  43383  caucvgbf  44498  cvgcaule  44500  climsuse  44622  mullimc  44630  climf  44636  mullimcf  44637  idlimc  44640  limcperiod  44642  clim2f  44650  limcleqr  44658  limclner  44665  climf2  44680  clim2f2  44684  fnlimabslt  44693  climuz  44758  fperdvper  44933  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  dvnmul  44957  stoweidlem9  45023  wallispilem4  45082  wallispilem5  45083  dirkerval  45105  dirkerval2  45108  dirkertrigeqlem1  45112  dirkertrigeqlem2  45113  dirkertrigeq  45115  dirkercncflem2  45118  ovnhoi  45617  hspmbllem1  45640  digfval  47370  dignn0flhalflem2  47389