MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvoveq1d Structured version   Visualization version   GIF version

Theorem fvoveq1d 7380
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
StepHypRef Expression
1 fvoveq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21oveq1d 7373 . 2 (𝜑 → (𝐴𝑂𝐶) = (𝐵𝑂𝐶))
32fveq2d 6847 1 (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cfv 6497  (class class class)co 7358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  fvoveq1  7381  imbrov2fvoveq  7383  hashfzp1  14332  pfxfvlsw  14584  swrdswrd  14594  revrev  14656  cshwidx0mod  14694  2cshw  14702  lswcshw  14704  cshweqrep  14710  cshimadifsn0  14720  lswco  14729  cau3lem  15240  clim  15377  rlim  15378  rlim2  15379  clim2  15387  rlimclim  15429  climrlim2  15430  climshftlem  15457  rlimcn3  15473  climcn2  15476  subcn2  15478  isercoll  15553  climcau  15556  caurcvg2  15563  caucvgb  15565  iseralt  15570  climcndslem1  15735  smumullem  16373  prmreclem4  16792  cshwsidrepsw  16967  efgredlem  19530  islmhm2  20502  coe1pwmul  21653  coe1sclmul  21656  evl1gsumadd  21727  chfacfscmulgsum  22212  chfacfpmmulgsum  22216  mulc1cncf  24271  pcovalg  24378  ehl1eudisval  24788  ovolunlem1a  24863  ovolunlem1  24864  mbfi1fseq  25089  isibl  25133  isibl2  25134  cbvitg  25143  itgeqa  25181  dveflem  25346  dvferm1lem  25351  dvferm1  25352  dvferm2lem  25353  dvferm2  25354  dvlip  25360  c1lip1  25364  lhop1lem  25380  lhop1  25381  ftc1lem5  25407  vieta1lem2  25674  aalioulem3  25697  ulmshftlem  25751  ulmcaulem  25756  ulmcau  25757  ulmdvlem3  25764  rlimcnp  26318  scvxcvx  26338  jensenlem2  26340  lgamgulmlem2  26382  lgamgulmlem5  26385  lgamgulm2  26388  lgamcvglem  26392  lgamcvg2  26407  basellem4  26436  basellem5  26437  pcbcctr  26627  dchrisumlem3  26842  dchrmusumlema  26844  dchrmusum2  26845  dchrvmasumlem2  26849  dchrvmasumlema  26851  dchrvmasumiflem1  26852  dchrisum0lema  26865  dchrisum0lem1b  26866  dchrisum0lem2  26869  dchrisum0  26871  chpdifbndlem1  26904  selbergsb  26926  pntlemo  26958  crctcshwlkn0lem2  28759  crctcshwlkn0lem3  28760  crctcshlem4  28768  crctcsh  28772  clwwisshclwwslemlem  28960  lnolin  29699  lnoadd  29703  norm3adifi  30098  lnopl  30859  lnfnl  30876  lnopaddi  30916  lnfnaddi  30988  pfxlsw2ccat  31809  lmatfval  32398  xrge0iifhom  32521  itgeq12dv  32929  signsply0  33166  revwlk  33721  snmlval  33928  iprodgam  34318  knoppcnlem1  34959  knoppndvlem21  34998  matunitlindflem1  36077  poimirlem29  36110  poimirlem32  36113  itg2addnclem3  36134  ftc1cnnc  36153  ftc1anclem6  36159  ftc1anclem7  36160  geomcau  36221  lfli  37526  lfladd  37531  docavalN  39589  diaocN  39591  dihjatc  39883  dvh4dimat  39904  sticksstones10  40566  sticksstones12a  40568  irrapxlem3  41150  irrapxlem4  41151  pellexlem6  41160  rmxfval  41230  rmyfval  41231  hashnzfz  42607  hashnzfzclim  42609  caucvgbf  43732  cvgcaule  43734  climsuse  43856  mullimc  43864  climf  43870  mullimcf  43871  idlimc  43874  limcperiod  43876  clim2f  43884  limcleqr  43892  limclner  43899  climf2  43914  clim2f2  43918  fnlimabslt  43927  climuz  43992  fperdvper  44167  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvnmul  44191  stoweidlem9  44257  wallispilem4  44316  wallispilem5  44317  dirkerval  44339  dirkerval2  44342  dirkertrigeqlem1  44346  dirkertrigeqlem2  44347  dirkertrigeq  44349  dirkercncflem2  44352  ovnhoi  44851  hspmbllem1  44874  digfval  46690  dignn0flhalflem2  46709
  Copyright terms: Public domain W3C validator