Theorem fvoveq1d 7446

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ‘cfv 6543  (class class class)co 7424

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427

This theorem is used by:  fvoveq1  7447  imbrov2fvoveq  7449  hashfzp1  14583  pfxfvlsw  14852  swrdswrd  14862  revrev  14924  cshwidx0mod  14964  2cshw  14972  lswcshw  14974  cshweqrep  14980  cshimadifsn0  14989  lswco  14998  cau3lem  15531  clim  15670  rlim  15671  rlim2  15672  clim2  15680  rlimclim  15722  climrlim2  15723  climshftlem  15750  rlimcn3  15766  climcn2  15769  subcn2  15771  isercoll  15844  climcau  15847  caurcvg2  15854  caucvgb  15856  iseralt  15861  climcndslem1  16027  smumullem  16671  prmreclem4  17106  cshwsidrepsw  17280  efgredlem  19970  islmhm2  21322  coe1pwmul  22607  coe1sclmul  22610  evl1gsumadd  22685  matunitlindflem1  23003  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  mpomulcn  25197  mulc1cncf  25235  pcovalg  25342  ehl1eudisval  25751  ovolunlem1a  25826  ovolunlem1  25827  mbfi1fseq  26051  isibl  26095  isibl2  26096  cbvitg  26105  cbvitgv  26106  itgeqa  26143  dveflem  26308  dvferm1lem  26313  dvferm1  26314  dvferm2lem  26315  dvferm2  26316  dvlip  26322  c1lip1  26326  lhop1lem  26342  lhop1  26343  ftc1lem5  26369  vieta1lem2  26643  aalioulem3  26670  ulmshftlem  26725  ulmcaulem  26730  ulmcau  26731  ulmdvlem3  26738  rlimcnp  27302  scvxcvx  27322  jensenlem2  27324  lgamgulmlem2  27366  lgamgulmlem5  27369  lgamgulm2  27372  lgamcvglem  27376  lgamcvg2  27391  basellem4  27420  basellem5  27421  pcbcctr  27612  dchrisumlem3  27827  dchrmusumlema  27829  dchrmusum2  27830  dchrvmasumlem2  27834  dchrvmasumlema  27836  dchrvmasumiflem1  27837  dchrisum0lema  27850  dchrisum0lem1b  27851  dchrisum0lem2  27854  dchrisum0  27856  chpdifbndlem1  27889  selbergsb  27911  pntlemo  27943  revwlk  30276  crctcshwlkn0lem2  30409  crctcshwlkn0lem3  30410  crctcshlem4  30418  crctcsh  30422  clwwisshclwwslemlem  30613  lnolin  31365  lnoadd  31369  norm3adifi  31764  lnopl  32525  lnfnl  32542  lnopaddi  32582  lnfnaddi  32654  pfxlsw2ccat  33563  extvfval  34214  mplvrpmrhm  34229  constrrtlc1  34414  constrrtcc  34417  lmatfval  34496  xrge0iifhom  34619  itgeq12dv  35008  signsply0  35230  snmlval  36214  iprodgam  36631  cbvitgvw2  37161  cbvitgdavw  37194  cbvitgdavw2  37210  knoppcnlem1  37483  knoppndvlem21  37522  poimirlem29  38704  poimirlem32  38707  itg2addnclem3  38728  ftc1cnnc  38747  ftc1anclem6  38753  ftc1anclem7  38754  geomcau  38830  lfli  40255  lfladd  40260  docavalN  42317  diaocN  42319  dihjatc  42611  dvh4dimat  42632  sticksstones10  43342  sticksstones12a  43344  irrapxlem3  43968  irrapxlem4  43969  pellexlem6  43978  rmxfval  44048  rmyfval  44049  hashnzfz  45441  hashnzfzclim  45443  caucvgbf  46635  cvgcaule  46637  climsuse  46756  mullimc  46764  climf  46770  mullimcf  46771  idlimc  46774  limcperiod  46776  clim2f  46782  limcleqr  46790  limclner  46797  climf2  46812  clim2f2  46816  fnlimabslt  46825  climuz  46890  fperdvper  47065  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  dvnmul  47089  stoweidlem9  47155  wallispilem4  47214  wallispilem5  47215  dirkerval  47237  dirkerval2  47240  dirkertrigeqlem1  47244  dirkertrigeqlem2  47245  dirkertrigeq  47247  dirkercncflem2  47250  fourierdlem48  47300  fourierdlem49  47301  fourierdlem113  47365  ovnhoi  47749  hspmbllem1  47772  digfval  49845  dignn0flhalflem2  49864  dfinito4  50772  fuconuniqex2  50923  ranfval  50933