Theorem fvoveq1d 7441

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6540  (class class class)co 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  fvoveq1  7442  imbrov2fvoveq  7444  hashfzp1  14486  pfxfvlsw  14754  swrdswrd  14764  revrev  14826  cshwidx0mod  14866  2cshw  14874  lswcshw  14876  cshweqrep  14882  cshimadifsn0  14891  lswco  14900  cau3lem  15430  clim  15569  rlim  15570  rlim2  15571  clim2  15579  rlimclim  15621  climrlim2  15622  climshftlem  15649  rlimcn3  15665  climcn2  15668  subcn2  15670  isercoll  15743  climcau  15746  caurcvg2  15753  caucvgb  15755  iseralt  15760  climcndslem1  15926  smumullem  16572  prmreclem4  17001  cshwsidrepsw  17175  efgredlem  19861  islmhm2  21209  coe1pwmul  22490  coe1sclmul  22493  evl1gsumadd  22568  chfacfscmulgsum  23067  chfacfpmmulgsum  23071  mpomulcn  25077  mulc1cncf  25115  pcovalg  25222  ehl1eudisval  25631  ovolunlem1a  25706  ovolunlem1  25707  mbfi1fseq  25931  isibl  25975  isibl2  25976  cbvitg  25986  cbvitgv  25987  itgeqa  26024  dveflem  26189  dvferm1lem  26194  dvferm1  26195  dvferm2lem  26196  dvferm2  26197  dvlip  26203  c1lip1  26207  lhop1lem  26223  lhop1  26224  ftc1lem5  26250  vieta1lem2  26523  aalioulem3  26548  ulmshftlem  26603  ulmcaulem  26608  ulmcau  26609  ulmdvlem3  26616  rlimcnp  27181  scvxcvx  27201  jensenlem2  27203  lgamgulmlem2  27245  lgamgulmlem5  27248  lgamgulm2  27251  lgamcvglem  27255  lgamcvg2  27270  basellem4  27299  basellem5  27300  pcbcctr  27491  dchrisumlem3  27706  dchrmusumlema  27708  dchrmusum2  27709  dchrvmasumlem2  27713  dchrvmasumlema  27715  dchrvmasumiflem1  27716  dchrisum0lema  27729  dchrisum0lem1b  27730  dchrisum0lem2  27733  dchrisum0  27735  chpdifbndlem1  27768  selbergsb  27790  pntlemo  27822  revwlk  30094  crctcshwlkn0lem2  30227  crctcshwlkn0lem3  30228  crctcshlem4  30236  crctcsh  30240  clwwisshclwwslemlem  30431  lnolin  31177  lnoadd  31181  norm3adifi  31576  lnopl  32337  lnfnl  32354  lnopaddi  32394  lnfnaddi  32466  pfxlsw2ccat  33336  extvfval  33986  mplvrpmrhm  34001  constrrtlc1  34186  constrrtcc  34189  lmatfval  34268  xrge0iifhom  34391  itgeq12dv  34781  signsply0  35003  snmlval  35860  iprodgam  36271  cbvitgvw2  36817  cbvitgdavw  36850  cbvitgdavw2  36866  knoppcnlem1  37139  knoppndvlem21  37178  matunitlindflem1  38324  poimirlem29  38357  poimirlem32  38360  itg2addnclem3  38381  ftc1cnnc  38400  ftc1anclem6  38406  ftc1anclem7  38407  geomcau  38468  lfli  39893  lfladd  39898  docavalN  41955  diaocN  41957  dihjatc  42249  dvh4dimat  42270  sticksstones10  42980  sticksstones12a  42982  irrapxlem3  43609  irrapxlem4  43610  pellexlem6  43619  rmxfval  43689  rmyfval  43690  hashnzfz  45088  hashnzfzclim  45090  caucvgbf  46261  cvgcaule  46263  climsuse  46382  mullimc  46390  climf  46396  mullimcf  46397  idlimc  46400  limcperiod  46402  clim2f  46408  limcleqr  46416  limclner  46423  climf2  46438  clim2f2  46442  fnlimabslt  46451  climuz  46516  fperdvper  46691  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  dvnmul  46715  stoweidlem9  46781  wallispilem4  46840  wallispilem5  46841  dirkerval  46863  dirkerval2  46866  dirkertrigeqlem1  46870  dirkertrigeqlem2  46871  dirkertrigeq  46873  dirkercncflem2  46876  fourierdlem48  46926  fourierdlem49  46927  fourierdlem113  46991  ovnhoi  47375  hspmbllem1  47398  digfval  49434  dignn0flhalflem2  49453  dfinito4  50336  ranfval  50449