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

Theorem fvoveq1d 6899
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 6892 . 2 (𝜑 → (𝐴𝑂𝐶) = (𝐵𝑂𝐶))
32fveq2d 6415 1 (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cfv 6104  (class class class)co 6877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-iota 6067  df-fv 6112  df-ov 6880
This theorem is referenced by:  fvoveq1  6900  imbrov2fvoveq  6902  hashfzp1  13438  swrd0fvlsw  13670  swrdswrd  13687  revrev  13743  cshwidx0mod  13778  2cshw  13786  lswcshw  13788  cshweqrep  13794  cshimadifsn0  13803  lswco  13811  cau3lem  14320  clim  14451  rlim  14452  rlim2  14453  clim2  14461  rlimclim  14503  climrlim2  14504  climshftlem  14531  rlimcn2  14547  climcn2  14549  subcn2  14551  isercoll  14624  climcau  14627  caurcvg2  14634  caucvgb  14636  iseralt  14641  climcndslem1  14806  smumullem  15436  prmreclem4  15843  cshwsidrepsw  16015  efgredlem  18364  islmhm2  19248  coe1pwmul  19860  coe1sclmul  19863  evl1gsumadd  19933  chfacfscmulgsum  20882  chfacfpmmulgsum  20886  mulc1cncf  22925  pcovalg  23028  ovolunlem1a  23483  ovolunlem1  23484  mbfi1fseq  23708  isibl  23752  isibl2  23753  cbvitg  23762  itgeqa  23800  dveflem  23962  dvferm1lem  23967  dvferm1  23968  dvferm2lem  23969  dvferm2  23970  dvlip  23976  c1lip1  23980  lhop1lem  23996  lhop1  23997  ftc1lem5  24023  vieta1lem2  24286  aalioulem3  24309  ulmshftlem  24363  ulmcaulem  24368  ulmcau  24369  ulmdvlem3  24376  rlimcnp  24912  scvxcvx  24932  jensenlem2  24934  lgamgulmlem2  24976  lgamgulmlem5  24979  lgamgulm2  24982  lgamcvglem  24986  lgamcvg2  25001  basellem4  25030  basellem5  25031  pcbcctr  25221  dchrisumlem3  25400  dchrmusumlema  25402  dchrmusum2  25403  dchrvmasumlem2  25407  dchrvmasumlema  25409  dchrvmasumiflem1  25410  dchrisum0lema  25423  dchrisum0lem1b  25424  dchrisum0lem2  25427  dchrisum0  25429  chpdifbndlem1  25462  selbergsb  25484  pntlemo  25516  crctcshwlkn0lem2  26938  crctcshwlkn0lem3  26939  crctcshlem4  26947  crctcsh  26951  clwwisshclwwslemlem  27162  lnolin  27943  lnoadd  27947  norm3adifi  28344  lnopl  29107  lnfnl  29124  lnopaddi  29164  lnfnaddi  29236  lmatfval  30211  xrge0iifhom  30314  itgeq12dv  30719  signsply0  30959  snmlval  31641  iprodgam  31955  knoppcnlem1  32805  knoppndvlem21  32845  matunitlindflem1  33720  poimirlem29  33753  poimirlem32  33756  itg2addnclem3  33777  ftc1cnnc  33798  ftc1anclem6  33804  ftc1anclem7  33805  geomcau  33868  lfli  34843  lfladd  34848  docavalN  36905  diaocN  36907  dihjatc  37199  dvh4dimat  37220  irrapxlem3  37891  irrapxlem4  37892  pellexlem6  37901  rmxfval  37971  rmyfval  37972  hashnzfz  39020  hashnzfzclim  39022  climsuse  40321  mullimc  40329  climf  40335  mullimcf  40336  idlimc  40339  limcperiod  40341  clim2f  40349  limcleqr  40357  limclner  40364  climf2  40379  clim2f2  40383  fnlimabslt  40392  climuz  40457  fperdvper  40614  ioodvbdlimc1lem2  40628  ioodvbdlimc2lem  40630  dvnmul  40639  wallispilem4  40765  wallispilem5  40766  dirkerval  40788  dirkerval2  40791  dirkertrigeqlem1  40795  dirkertrigeqlem2  40796  dirkertrigeq  40798  dirkercncflem2  40801  ovnhoi  41300  hspmbllem1  41323  pfxfvlsw  41979  digfval  42960  dignn0flhalflem2  42979
  Copyright terms: Public domain W3C validator