Theorem fvoveq1d 7442

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-ov 7423

This theorem is used by:  fvoveq1  7443  imbrov2fvoveq  7445  hashfzp1  14576  pfxfvlsw  14844  swrdswrd  14854  revrev  14916  cshwidx0mod  14956  2cshw  14964  lswcshw  14966  cshweqrep  14972  cshimadifsn0  14981  lswco  14990  cau3lem  15522  clim  15661  rlim  15662  rlim2  15663  clim2  15671  rlimclim  15713  climrlim2  15714  climshftlem  15741  rlimcn3  15757  climcn2  15760  subcn2  15762  isercoll  15835  climcau  15838  caurcvg2  15845  caucvgb  15847  iseralt  15852  climcndslem1  16018  smumullem  16662  prmreclem4  17097  cshwsidrepsw  17271  efgredlem  19961  islmhm2  21313  coe1pwmul  22598  coe1sclmul  22601  evl1gsumadd  22676  matunitlindflem1  22994  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  mpomulcn  25188  mulc1cncf  25226  pcovalg  25333  ehl1eudisval  25742  ovolunlem1a  25817  ovolunlem1  25818  mbfi1fseq  26042  isibl  26086  isibl2  26087  cbvitg  26096  cbvitgv  26097  itgeqa  26134  dveflem  26299  dvferm1lem  26304  dvferm1  26305  dvferm2lem  26306  dvferm2  26307  dvlip  26313  c1lip1  26317  lhop1lem  26333  lhop1  26334  ftc1lem5  26360  vieta1lem2  26634  aalioulem3  26661  ulmshftlem  26716  ulmcaulem  26721  ulmcau  26722  ulmdvlem3  26729  rlimcnp  27293  scvxcvx  27313  jensenlem2  27315  lgamgulmlem2  27357  lgamgulmlem5  27360  lgamgulm2  27363  lgamcvglem  27367  lgamcvg2  27382  basellem4  27411  basellem5  27412  pcbcctr  27603  dchrisumlem3  27818  dchrmusumlema  27820  dchrmusum2  27821  dchrvmasumlem2  27825  dchrvmasumlema  27827  dchrvmasumiflem1  27828  dchrisum0lema  27841  dchrisum0lem1b  27842  dchrisum0lem2  27845  dchrisum0  27847  chpdifbndlem1  27880  selbergsb  27902  pntlemo  27934  revwlk  30267  crctcshwlkn0lem2  30400  crctcshwlkn0lem3  30401  crctcshlem4  30409  crctcsh  30413  clwwisshclwwslemlem  30604  lnolin  31356  lnoadd  31360  norm3adifi  31755  lnopl  32516  lnfnl  32533  lnopaddi  32573  lnfnaddi  32645  pfxlsw2ccat  33513  extvfval  34164  mplvrpmrhm  34179  constrrtlc1  34364  constrrtcc  34367  lmatfval  34446  xrge0iifhom  34569  itgeq12dv  34958  signsply0  35180  snmlval  36096  iprodgam  36507  cbvitgvw2  37037  cbvitgdavw  37070  cbvitgdavw2  37086  knoppcnlem1  37359  knoppndvlem21  37398  poimirlem29  38567  poimirlem32  38570  itg2addnclem3  38591  ftc1cnnc  38610  ftc1anclem6  38616  ftc1anclem7  38617  geomcau  38693  lfli  40118  lfladd  40123  docavalN  42180  diaocN  42182  dihjatc  42474  dvh4dimat  42495  sticksstones10  43205  sticksstones12a  43207  irrapxlem3  43830  irrapxlem4  43831  pellexlem6  43840  rmxfval  43910  rmyfval  43911  hashnzfz  45303  hashnzfzclim  45305  caucvgbf  46498  cvgcaule  46500  climsuse  46619  mullimc  46627  climf  46633  mullimcf  46634  idlimc  46637  limcperiod  46639  clim2f  46645  limcleqr  46653  limclner  46660  climf2  46675  clim2f2  46679  fnlimabslt  46688  climuz  46753  fperdvper  46928  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnmul  46952  stoweidlem9  47018  wallispilem4  47077  wallispilem5  47078  dirkerval  47100  dirkerval2  47103  dirkertrigeqlem1  47107  dirkertrigeqlem2  47108  dirkertrigeq  47110  dirkercncflem2  47113  fourierdlem48  47163  fourierdlem49  47164  fourierdlem113  47228  ovnhoi  47612  hspmbllem1  47635  digfval  49708  dignn0flhalflem2  49727  dfinito4  50608  ranfval  50721