Theorem fvoveq1d 7045

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

Syntax hints:   → wi 4   = wceq 1525  ‘cfv 6232  (class class class)co 7023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-iota 6196  df-fv 6240  df-ov 7026

This theorem is referenced by:  fvoveq1  7046  imbrov2fvoveq  7048  hashfzp1  13644  pfxfvlsw  13897  swrdswrd  13907  revrev  13969  cshwidx0mod  14007  2cshw  14015  lswcshw  14017  cshweqrep  14023  cshimadifsn0  14032  lswco  14041  cau3lem  14552  clim  14689  rlim  14690  rlim2  14691  clim2  14699  rlimclim  14741  climrlim2  14742  climshftlem  14769  rlimcn2  14785  climcn2  14787  subcn2  14789  isercoll  14862  climcau  14865  caurcvg2  14872  caucvgb  14874  iseralt  14879  climcndslem1  15041  smumullem  15678  prmreclem4  16088  cshwsidrepsw  16260  efgredlem  18604  islmhm2  19504  coe1pwmul  20134  coe1sclmul  20137  evl1gsumadd  20207  chfacfscmulgsum  21156  chfacfpmmulgsum  21160  mulc1cncf  23200  pcovalg  23303  ehl1eudisval  23711  ovolunlem1a  23784  ovolunlem1  23785  mbfi1fseq  24009  isibl  24053  isibl2  24054  cbvitg  24063  itgeqa  24101  dveflem  24263  dvferm1lem  24268  dvferm1  24269  dvferm2lem  24270  dvferm2  24271  dvlip  24277  c1lip1  24281  lhop1lem  24297  lhop1  24298  ftc1lem5  24324  vieta1lem2  24587  aalioulem3  24610  ulmshftlem  24664  ulmcaulem  24669  ulmcau  24670  ulmdvlem3  24677  rlimcnp  25229  scvxcvx  25249  jensenlem2  25251  lgamgulmlem2  25293  lgamgulmlem5  25296  lgamgulm2  25299  lgamcvglem  25303  lgamcvg2  25318  basellem4  25347  basellem5  25348  pcbcctr  25538  dchrisumlem3  25753  dchrmusumlema  25755  dchrmusum2  25756  dchrvmasumlem2  25760  dchrvmasumlema  25762  dchrvmasumiflem1  25763  dchrisum0lema  25776  dchrisum0lem1b  25777  dchrisum0lem2  25780  dchrisum0  25782  chpdifbndlem1  25815  selbergsb  25837  pntlemo  25869  crctcshwlkn0lem2  27275  crctcshwlkn0lem3  27276  crctcshlem4  27284  crctcsh  27288  clwwisshclwwslemlem  27477  lnolin  28218  lnoadd  28222  norm3adifi  28617  lnopl  29378  lnfnl  29395  lnopaddi  29435  lnfnaddi  29507  pfxlsw2ccat  30301  lmatfval  30690  xrge0iifhom  30793  itgeq12dv  31197  signsply0  31434  revwlk  31981  snmlval  32188  iprodgam  32584  knoppcnlem1  33443  knoppndvlem21  33482  matunitlindflem1  34440  poimirlem29  34473  poimirlem32  34476  itg2addnclem3  34497  ftc1cnnc  34518  ftc1anclem6  34524  ftc1anclem7  34525  geomcau  34587  lfli  35749  lfladd  35754  docavalN  37811  diaocN  37813  dihjatc  38105  dvh4dimat  38126  irrapxlem3  38927  irrapxlem4  38928  pellexlem6  38937  rmxfval  39007  rmyfval  39008  hashnzfz  40211  hashnzfzclim  40213  climsuse  41452  mullimc  41460  climf  41466  mullimcf  41467  idlimc  41470  limcperiod  41472  clim2f  41480  limcleqr  41488  limclner  41495  climf2  41510  clim2f2  41514  fnlimabslt  41523  climuz  41588  fperdvper  41766  ioodvbdlimc1lem2  41780  ioodvbdlimc2lem  41782  dvnmul  41791  stoweidlem9  41858  wallispilem4  41917  wallispilem5  41918  dirkerval  41940  dirkerval2  41943  dirkertrigeqlem1  41947  dirkertrigeqlem2  41948  dirkertrigeq  41950  dirkercncflem2  41953  ovnhoi  42449  hspmbllem1  42472  digfval  44160  dignn0flhalflem2  44179