Theorem fvoveq1d 7436

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417

This theorem is used by:  fvoveq1  7437  imbrov2fvoveq  7439  hashfzp1  14497  pfxfvlsw  14765  swrdswrd  14775  revrev  14837  cshwidx0mod  14877  2cshw  14885  lswcshw  14887  cshweqrep  14893  cshimadifsn0  14902  lswco  14911  cau3lem  15443  clim  15582  rlim  15583  rlim2  15584  clim2  15592  rlimclim  15634  climrlim2  15635  climshftlem  15662  rlimcn3  15678  climcn2  15681  subcn2  15683  isercoll  15756  climcau  15759  caurcvg2  15766  caucvgb  15768  iseralt  15773  climcndslem1  15939  smumullem  16583  prmreclem4  17012  cshwsidrepsw  17186  efgredlem  19875  islmhm2  21223  coe1pwmul  22506  coe1sclmul  22509  evl1gsumadd  22584  matunitlindflem1  22902  chfacfscmulgsum  23086  chfacfpmmulgsum  23090  mpomulcn  25096  mulc1cncf  25134  pcovalg  25241  ehl1eudisval  25650  ovolunlem1a  25725  ovolunlem1  25726  mbfi1fseq  25950  isibl  25994  isibl2  25995  cbvitg  26004  cbvitgv  26005  itgeqa  26042  dveflem  26207  dvferm1lem  26212  dvferm1  26213  dvferm2lem  26214  dvferm2  26215  dvlip  26221  c1lip1  26225  lhop1lem  26241  lhop1  26242  ftc1lem5  26268  vieta1lem2  26544  aalioulem3  26571  ulmshftlem  26626  ulmcaulem  26631  ulmcau  26632  ulmdvlem3  26639  rlimcnp  27203  scvxcvx  27223  jensenlem2  27225  lgamgulmlem2  27267  lgamgulmlem5  27270  lgamgulm2  27273  lgamcvglem  27277  lgamcvg2  27292  basellem4  27321  basellem5  27322  pcbcctr  27513  dchrisumlem3  27728  dchrmusumlema  27730  dchrmusum2  27731  dchrvmasumlem2  27735  dchrvmasumlema  27737  dchrvmasumiflem1  27738  dchrisum0lema  27751  dchrisum0lem1b  27752  dchrisum0lem2  27755  dchrisum0  27757  chpdifbndlem1  27790  selbergsb  27812  pntlemo  27844  revwlk  30147  crctcshwlkn0lem2  30280  crctcshwlkn0lem3  30281  crctcshlem4  30289  crctcsh  30293  clwwisshclwwslemlem  30484  lnolin  31236  lnoadd  31240  norm3adifi  31635  lnopl  32396  lnfnl  32413  lnopaddi  32453  lnfnaddi  32525  pfxlsw2ccat  33393  extvfval  34043  mplvrpmrhm  34058  constrrtlc1  34243  constrrtcc  34246  lmatfval  34325  xrge0iifhom  34448  itgeq12dv  34838  signsply0  35060  snmlval  35911  iprodgam  36322  cbvitgvw2  36869  cbvitgdavw  36902  cbvitgdavw2  36918  knoppcnlem1  37191  knoppndvlem21  37230  poimirlem29  38399  poimirlem32  38402  itg2addnclem3  38423  ftc1cnnc  38442  ftc1anclem6  38448  ftc1anclem7  38449  geomcau  38510  lfli  39935  lfladd  39940  docavalN  41997  diaocN  41999  dihjatc  42291  dvh4dimat  42312  sticksstones10  43022  sticksstones12a  43024  irrapxlem3  43666  irrapxlem4  43667  pellexlem6  43676  rmxfval  43746  rmyfval  43747  hashnzfz  45145  hashnzfzclim  45147  caucvgbf  46318  cvgcaule  46320  climsuse  46439  mullimc  46447  climf  46453  mullimcf  46454  idlimc  46457  limcperiod  46459  clim2f  46465  limcleqr  46473  limclner  46480  climf2  46495  clim2f2  46499  fnlimabslt  46508  climuz  46573  fperdvper  46748  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  dvnmul  46772  stoweidlem9  46838  wallispilem4  46897  wallispilem5  46898  dirkerval  46920  dirkerval2  46923  dirkertrigeqlem1  46927  dirkertrigeqlem2  46928  dirkertrigeq  46930  dirkercncflem2  46933  fourierdlem48  46983  fourierdlem49  46984  fourierdlem113  47048  ovnhoi  47432  hspmbllem1  47455  digfval  49528  dignn0flhalflem2  49547  dfinito4  50428  ranfval  50541