Theorem fvoveq1d 7432

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

Syntax hints:   → wi 4   = wceq 1570  ‘cfv 6536  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  fvoveq1  7433  imbrov2fvoveq  7435  hashfzp1  14464  pfxfvlsw  14728  swrdswrd  14738  revrev  14800  cshwidx0mod  14838  2cshw  14846  lswcshw  14848  cshweqrep  14854  cshimadifsn0  14863  lswco  14872  cau3lem  15402  clim  15541  rlim  15542  rlim2  15543  clim2  15551  rlimclim  15593  climrlim2  15594  climshftlem  15621  rlimcn3  15637  climcn2  15640  subcn2  15642  isercoll  15715  climcau  15718  caurcvg2  15725  caucvgb  15727  iseralt  15732  climcndslem1  15899  smumullem  16545  prmreclem4  16974  cshwsidrepsw  17148  efgredlem  19812  islmhm2  21159  coe1pwmul  22440  coe1sclmul  22443  evl1gsumadd  22518  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  mpomulcn  25026  mulc1cncf  25064  pcovalg  25171  ehl1eudisval  25580  ovolunlem1a  25655  ovolunlem1  25656  mbfi1fseq  25880  isibl  25924  isibl2  25925  cbvitg  25935  cbvitgv  25936  itgeqa  25973  dveflem  26138  dvferm1lem  26143  dvferm1  26144  dvferm2lem  26145  dvferm2  26146  dvlip  26152  c1lip1  26156  lhop1lem  26172  lhop1  26173  ftc1lem5  26199  vieta1lem2  26472  aalioulem3  26497  ulmshftlem  26552  ulmcaulem  26557  ulmcau  26558  ulmdvlem3  26565  rlimcnp  27130  scvxcvx  27150  jensenlem2  27152  lgamgulmlem2  27194  lgamgulmlem5  27197  lgamgulm2  27200  lgamcvglem  27204  lgamcvg2  27219  basellem4  27248  basellem5  27249  pcbcctr  27440  dchrisumlem3  27655  dchrmusumlema  27657  dchrmusum2  27658  dchrvmasumlem2  27662  dchrvmasumlema  27664  dchrvmasumiflem1  27665  dchrisum0lema  27678  dchrisum0lem1b  27679  dchrisum0lem2  27682  dchrisum0  27684  chpdifbndlem1  27717  selbergsb  27739  pntlemo  27771  crctcshwlkn0lem2  30160  crctcshwlkn0lem3  30161  crctcshlem4  30169  crctcsh  30173  clwwisshclwwslemlem  30364  lnolin  31106  lnoadd  31110  norm3adifi  31505  lnopl  32266  lnfnl  32283  lnopaddi  32323  lnfnaddi  32395  pfxlsw2ccat  33270  extvfval  33922  mplvrpmrhm  33937  constrrtlc1  34122  constrrtcc  34125  lmatfval  34204  xrge0iifhom  34327  itgeq12dv  34716  signsply0  34938  revwlk  35617  snmlval  35823  iprodgam  36234  cbvitgvw2  36760  cbvitgdavw  36793  cbvitgdavw2  36809  knoppcnlem1  37082  knoppndvlem21  37121  matunitlindflem1  38267  poimirlem29  38300  poimirlem32  38303  itg2addnclem3  38324  ftc1cnnc  38343  ftc1anclem6  38349  ftc1anclem7  38350  geomcau  38410  lfli  39835  lfladd  39840  docavalN  41897  diaocN  41899  dihjatc  42191  dvh4dimat  42212  sticksstones10  42922  sticksstones12a  42924  irrapxlem3  43551  irrapxlem4  43552  pellexlem6  43561  rmxfval  43631  rmyfval  43632  hashnzfz  45030  hashnzfzclim  45032  caucvgbf  46203  cvgcaule  46205  climsuse  46324  mullimc  46332  climf  46338  mullimcf  46339  idlimc  46342  limcperiod  46344  clim2f  46350  limcleqr  46358  limclner  46365  climf2  46380  clim2f2  46384  fnlimabslt  46393  climuz  46458  fperdvper  46633  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnmul  46657  stoweidlem9  46723  wallispilem4  46782  wallispilem5  46783  dirkerval  46805  dirkerval2  46808  dirkertrigeqlem1  46812  dirkertrigeqlem2  46813  dirkertrigeq  46815  dirkercncflem2  46818  fourierdlem48  46868  fourierdlem49  46869  fourierdlem113  46933  ovnhoi  47317  hspmbllem1  47340  digfval  49377  dignn0flhalflem2  49396  dfinito4  50279  ranfval  50392