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

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

Proof of Theorem fvoveq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21fvoveq1d 6894 1 (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cfv 6099  (class class class)co 6872
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 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782
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 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-rex 3100  df-rab 3103  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4843  df-iota 6062  df-fv 6107  df-ov 6875
This theorem is referenced by:  eluzadd  11931  eluzsub  11932  fldiv4p1lem1div2  12858  fldiv4lem1div2  12860  modval  12892  seqval  13033  seqp1  13037  seqshft2  13048  monoord  13052  monoord2  13053  seqhomo  13069  facp1  13283  faclbnd4lem2  13299  bcval  13309  lsw0  13562  ccatval1  13572  ccatval2  13573  ccatalpha  13588  swrdfv  13645  2swrd2eqwrdeq  13919  imval  14068  recan  14297  rlimcld2  14530  rlimcn1  14540  rlimcn2  14542  climcn1  14543  climcn2  14544  subcn2  14546  o1of2  14564  isercoll2  14620  climsup  14621  serf0  14632  iseraltlem2  14634  fsumrelem  14759  mertenslem1  14835  mertenslem2  14836  mertens  14837  bitsfval  15362  smuval  15420  pcfac  15818  vdwlem6  15905  vdwlem8  15907  vdwlem9  15908  vdwlem10  15909  imasaddvallem  16392  imasvscafn  16400  imasvscaval  16401  mhmlin  17545  mhmlem  17738  mulginvcom  17767  mhmmulg  17783  ghmlin  17865  efgsdm  18342  efgsdmi  18344  efgsrel  18346  efgsp1  18349  frgpup1  18387  abvmul  19031  abvtri  19032  issrngd  19063  lmhmlin  19240  psrmulval  19593  coe1mul2  19845  coe1tmmul2fv  19854  coe1pwmulfv  19856  cply1mul  19870  ipcj  20187  mat1scmat  20554  mdetmul  20638  madufval  20652  cramer0  20707  cpmatmcllem  20734  d1mat2pmat  20755  m2cpminvid2lem  20770  decpmatmullem  20787  decpmatmulsumfsupp  20789  pm2mpmhmlem1  20834  pm2mpmhmlem2  20835  cayhamlem1  20882  cpmadumatpoly  20899  cayleyhamilton  20906  1stcelcls  21476  imasdsf1olem  22389  comet  22529  nrmmetd  22590  tngngp  22669  tngngp3  22671  nmvs  22691  mulc1cncf  22919  cncfco  22921  pi1xfr  23065  pi1coghm  23071  caubl  23316  caublcls  23317  bcthlem2  23332  bcthlem3  23333  bcthlem4  23334  bcthlem5  23335  ivthlem2  23431  ovolicc2lem4  23499  volsuplem  23534  volsup  23535  uniioombllem3  23564  itg1climres  23693  itg2monolem1  23729  itg2i1fseqle  23733  itg2i1fseq  23734  itg2i1fseq2  23735  itg2addlem  23737  itgeq2  23756  dvferm1lem  23959  dvferm2lem  23961  dvlip  23968  c1lip1  23972  lhop1lem  23988  lhop1  23989  ftc1lem4  24014  ftc1lem6  24016  mdegmullem  24050  coe1mul3  24071  ply1divex  24108  coeeu  24193  coeeq  24195  coemullem  24218  coemul  24220  dvply1  24251  dvply2g  24252  aalioulem3  24301  aaliou3lem8  24312  ulmshftlem  24355  ulmshft  24356  ulmss  24363  pserdvlem2  24394  cxpcn3lem  24700  loglesqrt  24711  birthdaylem2  24891  emcllem2  24935  emcllem3  24936  harmonicbnd2  24943  lgamgulmlem2  24968  lgamgulmlem3  24969  lgamgulmlem5  24971  lgambdd  24975  lgamcvglem  24978  facgam  25004  ftalem7  25017  bposlem7  25227  bposlem9  25229  lgsqrlem2  25284  lgsqrlem4  25286  2lgslem3a  25333  2lgslem3b  25334  2lgslem3c  25335  2lgslem3d  25336  rplogsumlem1  25385  dchrvmasumlem1  25396  logsqvma  25443  logsqvma2  25444  selberglem3  25448  selberg  25449  selberg2lem  25451  selberg4lem1  25461  pntrsumo1  25466  selberg34r  25472  pntsval  25473  pntsval2  25477  pntrlog2bndlem1  25478  pntrlog2bndlem4  25481  pntpbnd  25489  pntibnd  25494  pntlemo  25508  ewlkinedg  26726  wkslem1  26729  uspgr2wlkeq  26768  wlkp1lem8  26803  wlkdlem2  26806  upgrwlkdvdelem  26858  crctcshwlkn0lem2  26930  crctcshwlkn0lem3  26931  crctcshwlkn0lem4  26932  crctcshwlkn0lem5  26933  wlkiswwlks2lem2  26995  wlkiswwlks2lem5  26998  wwlksnext  27028  wwlksnredwwlkn  27030  wwlksnextproplem2  27046  clwwlkccatlem  27130  clwlkclwwlklem2a1  27133  clwlkclwwlklem2fv1  27136  clwlkclwwlklem2a4  27138  clwlkclwwlklem2a  27139  clwlkclwwlklem2  27141  clwwisshclwwslemlem  27154  clwwisshclwws  27156  clwwlknlbonbgr1  27186  clwwlkel  27193  clwwlkf  27194  clwwlkwwlksb  27202  clwwlkext2edg  27204  wwlksext2clwwlk  27205  clwwlknonex2lem2  27275  eupthseg  27377  upgreupthseg  27380  eupth2lem3  27407  2clwwlk2clwwlklem  27521  2clwwlk  27522  numclwwlk1lem2f1  27534  numclwlk1lem2  27548  nvs  27844  nvtri  27851  ipval  27884  blocnilem  27985  phpar2  28004  phpar  28005  sii  28035  normsub0  28319  norm-ii  28321  norm-iii  28323  normsub  28326  normpyth  28328  norm3dif  28333  norm3lemt  28335  norm3adifi  28336  normpar  28338  polid  28342  bcs  28364  pjaddi  28871  pjsubi  28873  pjmuli  28874  pjcjt2  28877  lnopeq0lem2  29191  lnopunilem2  29196  branmfn  29290  hstel2  29404  stj  29420  cdj3lem1  29619  cdj3lem2b  29622  cdj3lem3b  29625  cdj3i  29626  cnre2csqlem  30279  cnre2csqima  30280  mndpluscn  30295  lmdvg  30322  plymulx  30948  signsvfn  30982  subfacval2  31490  cvmliftlem7  31594  elmrsubrn  31738  faclim2  31954  fwddifval  32588  fwddifnval  32589  dnival  32776  unblimceq0lem  32812  unbdqndv2  32817  matunitlindf  33718  poimirlem32  33752  itg2gt0cn  33775  ftc1cnnclem  33793  ftc1cnnc  33794  areacirc  33815  sdclem1  33848  fdc  33850  seqpo  33852  incsequz  33853  incsequz2  33854  mettrifi  33862  caushft  33866  bfplem1  33930  ghomco  33999  rngohomadd  34077  rngohommul  34078  dihval  37011  lclkrlem1  37285  hdmap14lem2a  37646  hgmapval  37666  incssnn0  37774  rencldnfilem  37884  irrapxlem5  37890  irrapxlem6  37891  pellexlem3  37895  cvgdvgrat  39010  radcnvrat  39011  hashnzfzclim  39019  binomcxplemradcnv  39049  iunincfi  39763  monoords  39990  fperiodmullem  39996  monoordxrv  40189  monoordxr  40190  monoord2xrv  40191  monoord2xr  40192  climinf  40316  climsuse  40318  climinff  40321  mullimc  40326  mullimcf  40333  idlimc  40336  limcperiod  40338  limcrecl  40339  limclner  40361  climinf2  40417  climxrrelem  40459  cnrefiisplem  40533  cnrefiisp  40534  climxlim2lem  40549  cncfshift  40565  cncfperiod  40570  fperdvper  40611  dvnmul  40636  iblspltprt  40666  itgspltprt  40672  itgiccshift  40673  itgperiod  40674  dirkerval2  40788  dirkertrigeqlem1  40792  dirkertrigeqlem2  40793  dirkertrigeqlem3  40794  dirkercncflem2  40798  dirkercncflem3  40799  elaa2lem  40927  elaa2  40928  nnfoctbdj  41150  meaiuninclem  41174  meaiunincf  41177  meaiuninc3v  41178  meaiuninc3  41179  meaiininclem  41180  meaiininc  41181  smflimlem6  41464  smonoord  41914  iccpartimp  41926  iccelpart  41942  icceuelpart  41945  fargshiftfv  41948  fmtnorec2  42028  bgoldbtbndlem2  42267  bgoldbtbndlem3  42268  bgoldbtbnd  42270  mgmhmlin  42352  rnghmmul  42466  c0snmgmhm  42480  zrrnghm  42483  ply1mulgsumlem3  42742  ply1mulgsumlem4  42743  ply1mulgsum  42744
  Copyright terms: Public domain W3C validator