Theorem fvoveq1d 7380

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6492  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  fvoveq1  7381  imbrov2fvoveq  7383  hashfzp1  14354  pfxfvlsw  14618  swrdswrd  14628  revrev  14690  cshwidx0mod  14728  2cshw  14736  lswcshw  14738  cshweqrep  14744  cshimadifsn0  14753  lswco  14762  cau3lem  15278  clim  15417  rlim  15418  rlim2  15419  clim2  15427  rlimclim  15469  climrlim2  15470  climshftlem  15497  rlimcn3  15513  climcn2  15516  subcn2  15518  isercoll  15591  climcau  15594  caurcvg2  15601  caucvgb  15603  iseralt  15608  climcndslem1  15772  smumullem  16419  prmreclem4  16847  cshwsidrepsw  17021  efgredlem  19676  islmhm2  20990  coe1pwmul  22221  coe1sclmul  22224  evl1gsumadd  22302  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  mpomulcn  24814  mulc1cncf  24854  pcovalg  24968  ehl1eudisval  25377  ovolunlem1a  25453  ovolunlem1  25454  mbfi1fseq  25678  isibl  25722  isibl2  25723  cbvitg  25733  cbvitgv  25734  itgeqa  25771  dveflem  25939  dvferm1lem  25944  dvferm1  25945  dvferm2lem  25946  dvferm2  25947  dvlip  25954  c1lip1  25958  lhop1lem  25974  lhop1  25975  ftc1lem5  26003  vieta1lem2  26275  aalioulem3  26298  ulmshftlem  26354  ulmcaulem  26359  ulmcau  26360  ulmdvlem3  26367  rlimcnp  26931  scvxcvx  26952  jensenlem2  26954  lgamgulmlem2  26996  lgamgulmlem5  26999  lgamgulm2  27002  lgamcvglem  27006  lgamcvg2  27021  basellem4  27050  basellem5  27051  pcbcctr  27243  dchrisumlem3  27458  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumlema  27467  dchrvmasumiflem1  27468  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem2  27485  dchrisum0  27487  chpdifbndlem1  27520  selbergsb  27542  pntlemo  27574  crctcshwlkn0lem2  29884  crctcshwlkn0lem3  29885  crctcshlem4  29893  crctcsh  29897  clwwisshclwwslemlem  30088  lnolin  30829  lnoadd  30833  norm3adifi  31228  lnopl  31989  lnfnl  32006  lnopaddi  32046  lnfnaddi  32118  pfxlsw2ccat  33032  extvfval  33697  mplvrpmrhm  33712  constrrtlc1  33889  constrrtcc  33892  lmatfval  33971  xrge0iifhom  34094  itgeq12dv  34483  signsply0  34708  revwlk  35319  snmlval  35525  iprodgam  35936  cbvitgvw2  36442  cbvitgdavw  36475  cbvitgdavw2  36491  knoppcnlem1  36693  knoppndvlem21  36732  matunitlindflem1  37817  poimirlem29  37850  poimirlem32  37853  itg2addnclem3  37874  ftc1cnnc  37893  ftc1anclem6  37899  ftc1anclem7  37900  geomcau  37960  lfli  39321  lfladd  39326  docavalN  41383  diaocN  41385  dihjatc  41677  dvh4dimat  41698  sticksstones10  42409  sticksstones12a  42411  irrapxlem3  43066  irrapxlem4  43067  pellexlem6  43076  rmxfval  43146  rmyfval  43147  hashnzfz  44561  hashnzfzclim  44563  caucvgbf  45733  cvgcaule  45735  climsuse  45854  mullimc  45862  climf  45868  mullimcf  45869  idlimc  45872  limcperiod  45874  clim2f  45880  limcleqr  45888  limclner  45895  climf2  45910  clim2f2  45914  fnlimabslt  45923  climuz  45988  fperdvper  46163  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnmul  46187  stoweidlem9  46253  wallispilem4  46312  wallispilem5  46313  dirkerval  46335  dirkerval2  46338  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeq  46345  dirkercncflem2  46348  ovnhoi  46847  hspmbllem1  46870  digfval  48843  dignn0flhalflem2  48862  dfinito4  49746  ranfval  49859