Theorem fvoveq1d 7418

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

Syntax hints:   → wi 4   = wceq 1560  ‘cfv 6521  (class class class)co 7396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  fvoveq1  7419  imbrov2fvoveq  7421  hashfzp1  14444  pfxfvlsw  14708  swrdswrd  14718  revrev  14780  cshwidx0mod  14818  2cshw  14826  lswcshw  14828  cshweqrep  14834  cshimadifsn0  14843  lswco  14852  cau3lem  15382  clim  15521  rlim  15522  rlim2  15523  clim2  15531  rlimclim  15573  climrlim2  15574  climshftlem  15601  rlimcn3  15617  climcn2  15620  subcn2  15622  isercoll  15695  climcau  15698  caurcvg2  15705  caucvgb  15707  iseralt  15712  climcndslem1  15879  smumullem  16526  prmreclem4  16955  cshwsidrepsw  17129  efgredlem  19787  islmhm2  21105  coe1pwmul  22342  coe1sclmul  22345  evl1gsumadd  22421  chfacfscmulgsum  22920  chfacfpmmulgsum  22924  mpomulcn  24929  mulc1cncf  24967  pcovalg  25074  ehl1eudisval  25483  ovolunlem1a  25558  ovolunlem1  25559  mbfi1fseq  25783  isibl  25827  isibl2  25828  cbvitg  25838  cbvitgv  25839  itgeqa  25876  dveflem  26041  dvferm1lem  26046  dvferm1  26047  dvferm2lem  26048  dvferm2  26049  dvlip  26055  c1lip1  26059  lhop1lem  26075  lhop1  26076  ftc1lem5  26102  vieta1lem2  26375  aalioulem3  26398  ulmshftlem  26452  ulmcaulem  26457  ulmcau  26458  ulmdvlem3  26465  rlimcnp  27030  scvxcvx  27050  jensenlem2  27052  lgamgulmlem2  27094  lgamgulmlem5  27097  lgamgulm2  27100  lgamcvglem  27104  lgamcvg2  27119  basellem4  27148  basellem5  27149  pcbcctr  27340  dchrisumlem3  27555  dchrmusumlema  27557  dchrmusum2  27558  dchrvmasumlem2  27562  dchrvmasumlema  27564  dchrvmasumiflem1  27565  dchrisum0lema  27578  dchrisum0lem1b  27579  dchrisum0lem2  27582  dchrisum0  27584  chpdifbndlem1  27617  selbergsb  27639  pntlemo  27671  crctcshwlkn0lem2  30011  crctcshwlkn0lem3  30012  crctcshlem4  30020  crctcsh  30024  clwwisshclwwslemlem  30215  lnolin  30957  lnoadd  30961  norm3adifi  31356  lnopl  32117  lnfnl  32134  lnopaddi  32174  lnfnaddi  32246  pfxlsw2ccat  33128  extvfval  33829  mplvrpmrhm  33844  constrrtlc1  34029  constrrtcc  34032  lmatfval  34111  xrge0iifhom  34234  itgeq12dv  34623  signsply0  34845  revwlk  35475  snmlval  35681  iprodgam  36092  cbvitgvw2  36608  cbvitgdavw  36641  cbvitgdavw2  36657  knoppcnlem1  36931  knoppndvlem21  36970  matunitlindflem1  38115  poimirlem29  38148  poimirlem32  38151  itg2addnclem3  38172  ftc1cnnc  38191  ftc1anclem6  38197  ftc1anclem7  38198  geomcau  38258  lfli  39685  lfladd  39690  docavalN  41747  diaocN  41749  dihjatc  42041  dvh4dimat  42062  sticksstones10  42772  sticksstones12a  42774  irrapxlem3  43401  irrapxlem4  43402  pellexlem6  43411  rmxfval  43481  rmyfval  43482  hashnzfz  44896  hashnzfzclim  44898  caucvgbf  46063  cvgcaule  46065  climsuse  46184  mullimc  46192  climf  46198  mullimcf  46199  idlimc  46202  limcperiod  46204  clim2f  46210  limcleqr  46218  limclner  46225  climf2  46240  clim2f2  46244  fnlimabslt  46253  climuz  46318  fperdvper  46493  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnmul  46517  stoweidlem9  46583  wallispilem4  46642  wallispilem5  46643  dirkerval  46665  dirkerval2  46668  dirkertrigeqlem1  46672  dirkertrigeqlem2  46673  dirkertrigeq  46675  dirkercncflem2  46678  fourierdlem48  46728  fourierdlem49  46729  fourierdlem113  46793  ovnhoi  47177  hspmbllem1  47200  digfval  49219  dignn0flhalflem2  49238  dfinito4  50122  ranfval  50235