Theorem fvoveq1d 7473

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  fvoveq1  7474  imbrov2fvoveq  7476  hashfzp1  14617  pfxfvlsw  14886  swrdswrd  14896  revrev  14958  cshwidx0mod  14998  2cshw  15006  lswcshw  15008  cshweqrep  15014  cshimadifsn0  15023  lswco  15032  cau3lem  15566  clim  15705  rlim  15706  rlim2  15707  clim2  15715  rlimclim  15757  climrlim2  15758  climshftlem  15785  rlimcn3  15801  climcn2  15804  subcn2  15806  isercoll  15879  climcau  15882  caurcvg2  15889  caucvgb  15891  iseralt  15896  climcndslem1  16062  smumullem  16706  prmreclem4  17141  cshwsidrepsw  17315  efgredlem  20012  islmhm2  21364  coe1pwmul  22653  coe1sclmul  22656  evl1gsumadd  22731  matunitlindflem1  23049  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  mpomulcn  25243  mulc1cncf  25281  pcovalg  25388  ehl1eudisval  25797  ovolunlem1a  25872  ovolunlem1  25873  mbfi1fseq  26097  isibl  26141  isibl2  26142  cbvitg  26151  cbvitgv  26152  itgeqa  26189  dveflem  26354  dvferm1lem  26359  dvferm1  26360  dvferm2lem  26361  dvferm2  26362  dvlip  26368  c1lip1  26372  lhop1lem  26388  lhop1  26389  ftc1lem5  26415  vieta1lem2  26689  aalioulem3  26718  ulmshftlem  26773  ulmcaulem  26778  ulmcau  26779  ulmdvlem3  26786  rlimcnp  27350  scvxcvx  27370  jensenlem2  27372  lgamgulmlem2  27414  lgamgulmlem5  27417  lgamgulm2  27420  lgamcvglem  27424  lgamcvg2  27439  basellem4  27468  basellem5  27469  pcbcctr  27660  dchrisumlem3  27875  dchrmusumlema  27877  dchrmusum2  27878  dchrvmasumlem2  27882  dchrvmasumlema  27884  dchrvmasumiflem1  27885  dchrisum0lema  27898  dchrisum0lem1b  27899  dchrisum0lem2  27902  dchrisum0  27904  chpdifbndlem1  27937  selbergsb  27959  pntlemo  27991  revwlk  30324  crctcshwlkn0lem2  30457  crctcshwlkn0lem3  30458  crctcshlem4  30466  crctcsh  30470  clwwisshclwwslemlem  30661  lnolin  31413  lnoadd  31417  norm3adifi  31812  lnopl  32573  lnfnl  32590  lnopaddi  32630  lnfnaddi  32702  pfxlsw2ccat  33609  extvfval  34275  mplvrpmrhm  34290  constrrtlc1  34475  constrrtcc  34478  lmatfval  34557  xrge0iifhom  34680  itgeq12dv  35069  signsply0  35291  snmlval  36304  iprodgam  36722  cbvitgvw2  37252  cbvitgdavw  37285  cbvitgdavw2  37301  knoppcnlem1  37574  knoppndvlem21  37613  poimirlem29  38835  poimirlem32  38838  itg2addnclem3  38859  ftc1cnnc  38878  ftc1anclem6  38884  ftc1anclem7  38885  geomcau  38959  lfli  40384  lfladd  40389  docavalN  42446  diaocN  42448  dihjatc  42740  dvh4dimat  42761  sticksstones10  43471  sticksstones12a  43473  irrapxlem3  44097  irrapxlem4  44098  pellexlem6  44107  rmxfval  44177  rmyfval  44178  hashnzfz  45565  hashnzfzclim  45567  caucvgbf  46772  cvgcaule  46774  climsuse  46893  mullimc  46901  climf  46907  mullimcf  46908  idlimc  46911  limcperiod  46913  clim2f  46919  limcleqr  46927  limclner  46934  climf2  46949  clim2f2  46953  fnlimabslt  46962  climuz  47027  fperdvper  47202  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnmul  47226  stoweidlem9  47292  wallispilem4  47351  wallispilem5  47352  dirkerval  47374  dirkerval2  47377  dirkertrigeqlem1  47381  dirkertrigeqlem2  47382  dirkertrigeq  47384  dirkercncflem2  47387  fourierdlem48  47437  fourierdlem49  47438  fourierdlem113  47502  ovnhoi  47886  hspmbllem1  47909  digfval  50040  dignn0flhalflem2  50059  dfinito4  50967  fuconuniqex2  51118  ranfval  51128