Theorem fvoveq1 7158

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 7157. (Contributed by AV, 23-Jul-2022.)

Assertion

Ref	Expression
fvoveq1	⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Proof of Theorem fvoveq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fvoveq1d 7157	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1538  ‘cfv 6324  (class class class)co 7135

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  eluzadd  12261  eluzsub  12262  fldiv4p1lem1div2  13200  fldiv4lem1div2  13202  modval  13234  seqval  13375  seqp1  13379  seqshft2  13392  monoord  13396  monoord2  13397  seqhomo  13413  facp1  13634  faclbnd4lem2  13650  bcval  13660  lsw0  13908  ccatval1  13921  ccatval1OLD  13922  ccatval2  13923  ccatalpha  13938  swrdfv  14001  2swrd2eqwrdeq  14306  imval  14458  recan  14688  rlimcld2  14927  rlimcn1  14937  rlimcn2  14939  climcn1  14940  climcn2  14941  subcn2  14943  o1of2  14961  isercoll2  15017  climsup  15018  serf0  15029  iseraltlem2  15031  fsumrelem  15154  mertenslem1  15232  mertenslem2  15233  mertens  15234  bitsfval  15762  smuval  15820  pcfac  16225  vdwlem6  16312  vdwlem8  16314  vdwlem9  16315  vdwlem10  16316  imasaddvallem  16794  imasvscafn  16802  imasvscaval  16803  mhmlin  17955  mhmlem  18211  mulginvcom  18244  mhmmulg  18260  ghmlin  18355  efgsdm  18848  efgsdmi  18850  efgsrel  18852  efgsp1  18855  frgpup1  18893  abvmul  19593  abvtri  19594  issrngd  19625  lmhmlin  19800  ipcj  20323  psrmulval  20624  coe1mul2  20898  coe1tmmul2fv  20907  coe1pwmulfv  20909  cply1mul  20923  mat1scmat  21144  mdetmul  21228  madufval  21242  cramer0  21295  cpmatmcllem  21323  d1mat2pmat  21344  m2cpminvid2lem  21359  decpmatmullem  21376  decpmatmulsumfsupp  21378  pm2mpmhmlem1  21423  pm2mpmhmlem2  21424  cayhamlem1  21471  cpmadumatpoly  21488  cayleyhamilton  21495  1stcelcls  22066  imasdsf1olem  22980  comet  23120  nrmmetd  23181  tngngp  23260  tngngp3  23262  nmvs  23282  mulc1cncf  23510  cncfco  23512  pi1xfr  23660  pi1coghm  23666  caubl  23912  caublcls  23913  bcthlem2  23929  bcthlem3  23930  bcthlem4  23931  bcthlem5  23932  ivthlem2  24056  ovolicc2lem4  24124  volsuplem  24159  volsup  24160  uniioombllem3  24189  itg1climres  24318  itg2monolem1  24354  itg2i1fseqle  24358  itg2i1fseq  24359  itg2i1fseq2  24360  itg2addlem  24362  itgeq2  24381  dvferm1lem  24587  dvferm2lem  24589  dvlip  24596  c1lip1  24600  lhop1lem  24616  lhop1  24617  ftc1lem4  24642  ftc1lem6  24644  mdegmullem  24679  coe1mul3  24700  ply1divex  24737  coeeu  24822  coeeq  24824  coemullem  24847  coemul  24849  dvply1  24880  dvply2g  24881  aalioulem3  24930  aaliou3lem8  24941  ulmshftlem  24984  ulmshft  24985  ulmss  24992  pserdvlem2  25023  cxpcn3lem  25336  loglesqrt  25347  birthdaylem2  25538  emcllem2  25582  emcllem3  25583  harmonicbnd2  25590  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem5  25618  lgambdd  25622  lgamcvglem  25625  facgam  25651  ftalem7  25664  bposlem7  25874  bposlem9  25876  lgsqrlem2  25931  lgsqrlem4  25933  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  rplogsumlem1  26068  dchrvmasumlem1  26079  logsqvma  26126  logsqvma2  26127  selberglem3  26131  selberg  26132  selberg2lem  26134  selberg4lem1  26144  pntrsumo1  26149  selberg34r  26155  pntsval  26156  pntsval2  26160  pntrlog2bndlem1  26161  pntrlog2bndlem4  26164  pntpbnd  26172  pntibnd  26177  pntlemo  26191  ewlkinedg  27394  wkslem1  27397  uspgr2wlkeq  27435  wlkdlem2  27473  upgrwlkdvdelem  27525  crctcshwlkn0lem2  27597  crctcshwlkn0lem3  27598  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  wlkiswwlks2lem2  27656  wlkiswwlks2lem5  27659  wwlksnext  27679  wwlksnredwwlkn  27681  wwlksnextproplem2  27696  clwwlkccatlem  27774  clwlkclwwlklem2a1  27777  clwlkclwwlklem2fv1  27780  clwlkclwwlklem2a4  27782  clwlkclwwlklem2a  27783  clwlkclwwlklem2  27785  clwwisshclwwslemlem  27798  clwwisshclwws  27800  clwwlknlbonbgr1  27824  clwwlkel  27831  clwwlkf  27832  clwwlkwwlksb  27839  clwwlkext2edg  27841  wwlksext2clwwlk  27842  clwwlknonex2lem2  27893  eupthseg  27991  upgreupthseg  27994  eupth2lem3  28021  2clwwlk2clwwlklem  28131  2clwwlk  28132  numclwwlk1lem2f1  28142  numclwlk1lem2  28155  nvs  28446  nvtri  28453  ipval  28486  blocnilem  28587  phpar2  28606  phpar  28607  sii  28637  normsub0  28919  norm-ii  28921  norm-iii  28923  normsub  28926  normpyth  28928  norm3dif  28933  norm3lemt  28935  norm3adifi  28936  normpar  28938  polid  28942  bcs  28964  pjaddi  29469  pjsubi  29471  pjmuli  29472  pjcjt2  29475  lnopeq0lem2  29789  lnopunilem2  29794  branmfn  29888  hstel2  30002  stj  30018  cdj3lem1  30217  cdj3lem2b  30220  cdj3lem3b  30223  cdj3i  30224  cnre2csqlem  31263  cnre2csqima  31264  mndpluscn  31279  lmdvg  31306  plymulx  31928  signsvfn  31962  subfacval2  32547  cvmliftlem7  32651  elmrsubrn  32880  faclim2  33093  fwddifval  33736  fwddifnval  33737  dnival  33923  unblimceq0lem  33958  unbdqndv2  33963  matunitlindf  35055  poimirlem32  35089  itg2gt0cn  35112  ftc1cnnclem  35128  ftc1cnnc  35129  areacirc  35150  sdclem1  35181  fdc  35183  seqpo  35185  incsequz  35186  incsequz2  35187  mettrifi  35195  caushft  35199  bfplem1  35260  ghomco  35329  rngohomadd  35407  rngohommul  35408  dihval  38528  lclkrlem1  38802  hdmap14lem2a  39163  hgmapval  39183  fsuppind  39456  prjspnval  39610  incssnn0  39652  rencldnfilem  39761  irrapxlem5  39767  irrapxlem6  39768  pellexlem3  39772  cvgdvgrat  41017  radcnvrat  41018  hashnzfzclim  41026  binomcxplemradcnv  41056  iunincfi  41730  monoords  41929  fperiodmullem  41935  monoordxrv  42121  monoordxr  42122  monoord2xrv  42123  monoord2xr  42124  climinf  42248  climsuse  42250  climinff  42253  mullimc  42258  mullimcf  42265  idlimc  42268  limcperiod  42270  limcrecl  42271  limclner  42293  climinf2  42349  climxrrelem  42391  cnrefiisplem  42471  cnrefiisp  42472  climxlim2lem  42487  cncfshift  42516  cncfperiod  42521  fperdvper  42561  dvnmul  42585  iblspltprt  42615  itgspltprt  42621  itgiccshift  42622  itgperiod  42623  dirkerval2  42736  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkercncflem2  42746  dirkercncflem3  42747  fourierdlem29  42778  elaa2lem  42875  elaa2  42876  nnfoctbdj  43095  meaiuninclem  43119  meaiunincf  43122  meaiuninc3v  43123  meaiuninc3  43124  meaiininclem  43125  meaiininc  43126  smflimlem6  43409  smonoord  43888  iccpartimp  43934  iccelpart  43950  icceuelpart  43953  fargshiftfv  43956  fmtnorec2  44060  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbnd  44327  mgmhmlin  44406  rnghmmul  44524  c0snmgmhm  44538  zrrnghm  44541  ply1mulgsumlem3  44796  ply1mulgsumlem4  44797  ply1mulgsum  44798  ackvalsuc1  45093