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

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

Proof of Theorem fvoveq1
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21fvoveq1d 7172 1 (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  cfv 6354  (class class class)co 7150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6313  df-fv 6362  df-ov 7153
This theorem is referenced by:  eluzadd  12267  eluzsub  12268  fldiv4p1lem1div2  13200  fldiv4lem1div2  13202  modval  13234  seqval  13375  seqp1  13379  seqshft2  13391  monoord  13395  monoord2  13396  seqhomo  13412  facp1  13633  faclbnd4lem2  13649  bcval  13659  lsw0  13912  ccatval1  13925  ccatval1OLD  13926  ccatval2  13927  ccatalpha  13942  swrdfv  14005  2swrd2eqwrdeq  14310  imval  14461  recan  14691  rlimcld2  14930  rlimcn1  14940  rlimcn2  14942  climcn1  14943  climcn2  14944  subcn2  14946  o1of2  14964  isercoll2  15020  climsup  15021  serf0  15032  iseraltlem2  15034  fsumrelem  15157  mertenslem1  15235  mertenslem2  15236  mertens  15237  bitsfval  15767  smuval  15825  pcfac  16230  vdwlem6  16317  vdwlem8  16319  vdwlem9  16320  vdwlem10  16321  imasaddvallem  16797  imasvscafn  16805  imasvscaval  16806  mhmlin  17958  mhmlem  18164  mulginvcom  18197  mhmmulg  18213  ghmlin  18308  efgsdm  18792  efgsdmi  18794  efgsrel  18796  efgsp1  18799  frgpup1  18837  abvmul  19536  abvtri  19537  issrngd  19568  lmhmlin  19743  psrmulval  20101  coe1mul2  20372  coe1tmmul2fv  20381  coe1pwmulfv  20383  cply1mul  20397  ipcj  20713  mat1scmat  21083  mdetmul  21167  madufval  21181  cramer0  21234  cpmatmcllem  21261  d1mat2pmat  21282  m2cpminvid2lem  21297  decpmatmullem  21314  decpmatmulsumfsupp  21316  pm2mpmhmlem1  21361  pm2mpmhmlem2  21362  cayhamlem1  21409  cpmadumatpoly  21426  cayleyhamilton  21433  1stcelcls  22004  imasdsf1olem  22917  comet  23057  nrmmetd  23118  tngngp  23197  tngngp3  23199  nmvs  23219  mulc1cncf  23447  cncfco  23449  pi1xfr  23593  pi1coghm  23599  caubl  23845  caublcls  23846  bcthlem2  23862  bcthlem3  23863  bcthlem4  23864  bcthlem5  23865  ivthlem2  23987  ovolicc2lem4  24055  volsuplem  24090  volsup  24091  uniioombllem3  24120  itg1climres  24249  itg2monolem1  24285  itg2i1fseqle  24289  itg2i1fseq  24290  itg2i1fseq2  24291  itg2addlem  24293  itgeq2  24312  dvferm1lem  24515  dvferm2lem  24517  dvlip  24524  c1lip1  24528  lhop1lem  24544  lhop1  24545  ftc1lem4  24570  ftc1lem6  24572  mdegmullem  24606  coe1mul3  24627  ply1divex  24664  coeeu  24749  coeeq  24751  coemullem  24774  coemul  24776  dvply1  24807  dvply2g  24808  aalioulem3  24857  aaliou3lem8  24868  ulmshftlem  24911  ulmshft  24912  ulmss  24919  pserdvlem2  24950  cxpcn3lem  25260  loglesqrt  25271  birthdaylem2  25463  emcllem2  25507  emcllem3  25508  harmonicbnd2  25515  lgamgulmlem2  25540  lgamgulmlem3  25541  lgamgulmlem5  25543  lgambdd  25547  lgamcvglem  25550  facgam  25576  ftalem7  25589  bposlem7  25799  bposlem9  25801  lgsqrlem2  25856  lgsqrlem4  25858  2lgslem3a  25905  2lgslem3b  25906  2lgslem3c  25907  2lgslem3d  25908  rplogsumlem1  25993  dchrvmasumlem1  26004  logsqvma  26051  logsqvma2  26052  selberglem3  26056  selberg  26057  selberg2lem  26059  selberg4lem1  26069  pntrsumo1  26074  selberg34r  26080  pntsval  26081  pntsval2  26085  pntrlog2bndlem1  26086  pntrlog2bndlem4  26089  pntpbnd  26097  pntibnd  26102  pntlemo  26116  ewlkinedg  27319  wkslem1  27322  uspgr2wlkeq  27360  wlkdlem2  27398  upgrwlkdvdelem  27450  crctcshwlkn0lem2  27522  crctcshwlkn0lem3  27523  crctcshwlkn0lem4  27524  crctcshwlkn0lem5  27525  wlkiswwlks2lem2  27581  wlkiswwlks2lem5  27584  wwlksnext  27604  wwlksnredwwlkn  27606  wwlksnextproplem2  27622  clwwlkccatlem  27700  clwlkclwwlklem2a1  27703  clwlkclwwlklem2fv1  27706  clwlkclwwlklem2a4  27708  clwlkclwwlklem2a  27709  clwlkclwwlklem2  27711  clwwisshclwwslemlem  27724  clwwisshclwws  27726  clwwlknlbonbgr1  27750  clwwlkel  27758  clwwlkf  27759  clwwlkwwlksb  27766  clwwlkext2edg  27768  wwlksext2clwwlk  27769  clwwlknonex2lem2  27820  eupthseg  27918  upgreupthseg  27921  eupth2lem3  27948  2clwwlk2clwwlklem  28058  2clwwlk  28059  numclwwlk1lem2f1  28069  numclwlk1lem2  28082  nvs  28373  nvtri  28380  ipval  28413  blocnilem  28514  phpar2  28533  phpar  28534  sii  28564  normsub0  28846  norm-ii  28848  norm-iii  28850  normsub  28853  normpyth  28855  norm3dif  28860  norm3lemt  28862  norm3adifi  28863  normpar  28865  polid  28869  bcs  28891  pjaddi  29396  pjsubi  29398  pjmuli  29399  pjcjt2  29402  lnopeq0lem2  29716  lnopunilem2  29721  branmfn  29815  hstel2  29929  stj  29945  cdj3lem1  30144  cdj3lem2b  30147  cdj3lem3b  30150  cdj3i  30151  cnre2csqlem  31058  cnre2csqima  31059  mndpluscn  31074  lmdvg  31101  plymulx  31723  signsvfn  31757  subfacval2  32337  cvmliftlem7  32441  elmrsubrn  32670  faclim2  32883  fwddifval  33526  fwddifnval  33527  dnival  33713  unblimceq0lem  33748  unbdqndv2  33753  matunitlindf  34776  poimirlem32  34810  itg2gt0cn  34833  ftc1cnnclem  34851  ftc1cnnc  34852  areacirc  34873  sdclem1  34905  fdc  34907  seqpo  34909  incsequz  34910  incsequz2  34911  mettrifi  34919  caushft  34923  bfplem1  34987  ghomco  35056  rngohomadd  35134  rngohommul  35135  dihval  38254  lclkrlem1  38528  hdmap14lem2a  38889  hgmapval  38909  prjspnval  39150  incssnn0  39192  rencldnfilem  39301  irrapxlem5  39307  irrapxlem6  39308  pellexlem3  39312  cvgdvgrat  40529  radcnvrat  40530  hashnzfzclim  40538  binomcxplemradcnv  40568  iunincfi  41244  monoords  41448  fperiodmullem  41454  monoordxrv  41642  monoordxr  41643  monoord2xrv  41644  monoord2xr  41645  climinf  41771  climsuse  41773  climinff  41776  mullimc  41781  mullimcf  41788  idlimc  41791  limcperiod  41793  limcrecl  41794  limclner  41816  climinf2  41872  climxrrelem  41914  cnrefiisplem  41994  cnrefiisp  41995  climxlim2lem  42010  cncfshift  42041  cncfperiod  42046  fperdvper  42087  dvnmul  42112  iblspltprt  42142  itgspltprt  42148  itgiccshift  42149  itgperiod  42150  dirkerval2  42264  dirkertrigeqlem1  42268  dirkertrigeqlem2  42269  dirkertrigeqlem3  42270  dirkercncflem2  42274  dirkercncflem3  42275  fourierdlem29  42306  elaa2lem  42403  elaa2  42404  nnfoctbdj  42623  meaiuninclem  42647  meaiunincf  42650  meaiuninc3v  42651  meaiuninc3  42652  meaiininclem  42653  meaiininc  42654  smflimlem6  42937  smonoord  43416  iccpartimp  43428  iccelpart  43444  icceuelpart  43447  fargshiftfv  43450  fmtnorec2  43556  bgoldbtbndlem2  43822  bgoldbtbndlem3  43823  bgoldbtbnd  43825  mgmhmlin  43904  rnghmmul  44073  c0snmgmhm  44087  zrrnghm  44090  ply1mulgsumlem3  44344  ply1mulgsumlem4  44345  ply1mulgsum  44346
  Copyright terms: Public domain W3C validator