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

Theorem fvoveq1 7374
Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 7373. (Contributed by AV, 23-Jul-2022.)
Assertion
Ref Expression
fvoveq1 (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Proof of Theorem fvoveq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21fvoveq1d 7373 1 (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cfv 6493  (class class class)co 7351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-iota 6445  df-fv 6501  df-ov 7354
This theorem is referenced by:  eluzadd  12752  eluzsub  12753  fldiv4p1lem1div2  13694  fldiv4lem1div2  13696  modval  13730  seqval  13871  seqp1  13875  seqshft2  13888  monoord  13892  monoord2  13893  seqhomo  13909  facp1  14132  faclbnd4lem2  14148  bcval  14158  lsw0  14407  ccatval1  14419  ccatval2  14420  ccatalpha  14435  swrdfv  14494  2swrd2eqwrdeq  14800  imval  14952  recan  15181  rlimcld2  15420  rlimcn1  15430  rlimcn3  15432  climcn1  15434  climcn2  15435  subcn2  15437  o1of2  15455  isercoll2  15513  climsup  15514  serf0  15525  iseraltlem2  15527  fsumrelem  15652  mertenslem1  15729  mertenslem2  15730  mertens  15731  bitsfval  16263  smuval  16321  pcfac  16731  vdwlem6  16818  vdwlem8  16820  vdwlem9  16821  vdwlem10  16822  imasaddvallem  17371  imasvscafn  17379  imasvscaval  17380  mhmlin  18569  mhmlem  18826  mulginvcom  18860  mhmmulg  18876  ghmlin  18972  efgsdm  19471  efgsdmi  19473  efgsrel  19475  efgsp1  19478  frgpup1  19516  abvmul  20241  abvtri  20242  issrngd  20273  lmhmlin  20449  ipcj  20991  psrmulval  21307  mhpmulcl  21491  coe1mul2  21592  coe1tmmul2fv  21601  coe1pwmulfv  21603  cply1mul  21617  mat1scmat  21840  mdetmul  21924  madufval  21938  cramer0  21991  cpmatmcllem  22019  d1mat2pmat  22040  m2cpminvid2lem  22055  decpmatmullem  22072  decpmatmulsumfsupp  22074  pm2mpmhmlem1  22119  pm2mpmhmlem2  22120  cayhamlem1  22167  cpmadumatpoly  22184  cayleyhamilton  22191  1stcelcls  22764  imasdsf1olem  23678  comet  23821  nrmmetd  23882  tngngp  23970  tngngp3  23972  nmvs  23992  mulc1cncf  24220  cncfco  24222  pi1xfr  24370  pi1coghm  24376  caubl  24624  caublcls  24625  bcthlem2  24641  bcthlem3  24642  bcthlem4  24643  bcthlem5  24644  ivthlem2  24768  ovolicc2lem4  24836  volsuplem  24871  volsup  24872  uniioombllem3  24901  itg1climres  25031  itg2monolem1  25067  itg2i1fseqle  25071  itg2i1fseq  25072  itg2i1fseq2  25073  itg2addlem  25075  itgeq2  25094  dvferm1lem  25300  dvferm2lem  25302  dvlip  25309  c1lip1  25313  lhop1lem  25329  lhop1  25330  ftc1lem4  25355  ftc1lem6  25357  mdegmullem  25395  coe1mul3  25416  ply1divex  25453  coeeu  25538  coeeq  25540  coemullem  25563  coemul  25565  dvply1  25596  dvply2g  25597  aalioulem3  25646  aaliou3lem8  25657  ulmshftlem  25700  ulmshft  25701  ulmss  25708  pserdvlem2  25739  cxpcn3lem  26052  loglesqrt  26063  birthdaylem2  26254  emcllem2  26298  emcllem3  26299  harmonicbnd2  26306  lgamgulmlem2  26331  lgamgulmlem3  26332  lgamgulmlem5  26334  lgambdd  26338  lgamcvglem  26341  facgam  26367  ftalem7  26380  bposlem7  26590  bposlem9  26592  lgsqrlem2  26647  lgsqrlem4  26649  2lgslem3a  26696  2lgslem3b  26697  2lgslem3c  26698  2lgslem3d  26699  rplogsumlem1  26784  dchrvmasumlem1  26795  logsqvma  26842  logsqvma2  26843  selberglem3  26847  selberg  26848  selberg2lem  26850  selberg4lem1  26860  pntrsumo1  26865  selberg34r  26871  pntsval  26872  pntsval2  26876  pntrlog2bndlem1  26877  pntrlog2bndlem4  26880  pntpbnd  26888  pntibnd  26893  pntlemo  26907  ewlkinedg  28381  wkslem1  28384  uspgr2wlkeq  28423  wlkdlem2  28460  upgrwlkdvdelem  28513  crctcshwlkn0lem2  28585  crctcshwlkn0lem3  28586  crctcshwlkn0lem4  28587  crctcshwlkn0lem5  28588  wlkiswwlks2lem2  28644  wlkiswwlks2lem5  28647  wwlksnext  28667  wwlksnredwwlkn  28669  wwlksnextproplem2  28684  clwwlkccatlem  28762  clwlkclwwlklem2a1  28765  clwlkclwwlklem2fv1  28768  clwlkclwwlklem2a4  28770  clwlkclwwlklem2a  28771  clwlkclwwlklem2  28773  clwwisshclwwslemlem  28786  clwwisshclwws  28788  clwwlknlbonbgr1  28812  clwwlkel  28819  clwwlkf  28820  clwwlkwwlksb  28827  clwwlkext2edg  28829  wwlksext2clwwlk  28830  clwwlknonex2lem2  28881  eupthseg  28979  upgreupthseg  28982  eupth2lem3  29009  2clwwlk2clwwlklem  29119  2clwwlk  29120  numclwwlk1lem2f1  29130  numclwlk1lem2  29143  nvs  29434  nvtri  29441  ipval  29474  blocnilem  29575  phpar2  29594  phpar  29595  sii  29625  normsub0  29907  norm-ii  29909  norm-iii  29911  normsub  29914  normpyth  29916  norm3dif  29921  norm3lemt  29923  norm3adifi  29924  normpar  29926  polid  29930  bcs  29952  pjaddi  30457  pjsubi  30459  pjmuli  30460  pjcjt2  30463  lnopeq0lem2  30777  lnopunilem2  30782  branmfn  30876  hstel2  30990  stj  31006  cdj3lem1  31205  cdj3lem2b  31208  cdj3lem3b  31211  cdj3i  31212  cnre2csqlem  32303  cnre2csqima  32304  mndpluscn  32319  lmdvg  32346  plymulx  32972  signsvfn  33006  subfacval2  33593  cvmliftlem7  33697  elmrsubrn  33926  faclim2  34137  fwddifval  34685  fwddifnval  34686  dnival  34872  unblimceq0lem  34907  unbdqndv2  34912  matunitlindf  36014  poimirlem32  36048  itg2gt0cn  36071  ftc1cnnclem  36087  ftc1cnnc  36088  areacirc  36109  sdclem1  36140  fdc  36142  seqpo  36144  incsequz  36145  incsequz2  36146  mettrifi  36154  caushft  36158  bfplem1  36219  ghomco  36288  rngohomadd  36366  rngohommul  36367  dihval  39633  lclkrlem1  39907  hdmap14lem2a  40268  hgmapval  40288  sticksstones10  40501  sticksstones12a  40503  fsuppind  40674  prjspnval  40863  incssnn0  40943  rencldnfilem  41052  irrapxlem5  41058  irrapxlem6  41059  pellexlem3  41063  cvgdvgrat  42504  radcnvrat  42505  hashnzfzclim  42513  binomcxplemradcnv  42543  iunincfi  43215  monoords  43436  fperiodmullem  43442  monoordxrv  43622  monoordxr  43623  monoord2xrv  43624  monoord2xr  43625  climinf  43748  climsuse  43750  climinff  43753  mullimc  43758  mullimcf  43765  idlimc  43768  limcperiod  43770  limcrecl  43771  limclner  43793  climinf2  43849  climxrrelem  43891  cnrefiisplem  43971  cnrefiisp  43972  climxlim2lem  43987  cncfshift  44016  cncfperiod  44021  fperdvper  44061  dvnmul  44085  iblspltprt  44115  itgspltprt  44121  itgiccshift  44122  itgperiod  44123  dirkerval2  44236  dirkertrigeqlem1  44240  dirkertrigeqlem2  44241  dirkertrigeqlem3  44242  dirkercncflem2  44246  dirkercncflem3  44247  fourierdlem29  44278  elaa2lem  44375  elaa2  44376  nnfoctbdj  44598  meaiuninclem  44622  meaiunincf  44625  meaiuninc3v  44626  meaiuninc3  44627  meaiininclem  44628  meaiininc  44629  smflimlem6  44918  natglobalincr  45017  tworepnotupword  45026  smonoord  45464  iccpartimp  45510  iccelpart  45526  icceuelpart  45529  fargshiftfv  45532  fmtnorec2  45636  bgoldbtbndlem2  45899  bgoldbtbndlem3  45900  bgoldbtbnd  45902  mgmhmlin  45981  rnghmmul  46099  c0snmgmhm  46113  zrrnghm  46116  ply1mulgsumlem3  46370  ply1mulgsumlem4  46371  ply1mulgsum  46372  ackvalsuc1  46666
  Copyright terms: Public domain W3C validator