Theorem fvoveq1 7179

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 7178. (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 7178	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1537  ‘cfv 6355  (class class class)co 7156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  eluzadd  12274  eluzsub  12275  fldiv4p1lem1div2  13206  fldiv4lem1div2  13208  modval  13240  seqval  13381  seqp1  13385  seqshft2  13397  monoord  13401  monoord2  13402  seqhomo  13418  facp1  13639  faclbnd4lem2  13655  bcval  13665  lsw0  13917  ccatval1  13930  ccatval1OLD  13931  ccatval2  13932  ccatalpha  13947  swrdfv  14010  2swrd2eqwrdeq  14315  imval  14466  recan  14696  rlimcld2  14935  rlimcn1  14945  rlimcn2  14947  climcn1  14948  climcn2  14949  subcn2  14951  o1of2  14969  isercoll2  15025  climsup  15026  serf0  15037  iseraltlem2  15039  fsumrelem  15162  mertenslem1  15240  mertenslem2  15241  mertens  15242  bitsfval  15772  smuval  15830  pcfac  16235  vdwlem6  16322  vdwlem8  16324  vdwlem9  16325  vdwlem10  16326  imasaddvallem  16802  imasvscafn  16810  imasvscaval  16811  mhmlin  17963  mhmlem  18219  mulginvcom  18252  mhmmulg  18268  ghmlin  18363  efgsdm  18856  efgsdmi  18858  efgsrel  18860  efgsp1  18863  frgpup1  18901  abvmul  19600  abvtri  19601  issrngd  19632  lmhmlin  19807  psrmulval  20166  coe1mul2  20437  coe1tmmul2fv  20446  coe1pwmulfv  20448  cply1mul  20462  ipcj  20778  mat1scmat  21148  mdetmul  21232  madufval  21246  cramer0  21299  cpmatmcllem  21326  d1mat2pmat  21347  m2cpminvid2lem  21362  decpmatmullem  21379  decpmatmulsumfsupp  21381  pm2mpmhmlem1  21426  pm2mpmhmlem2  21427  cayhamlem1  21474  cpmadumatpoly  21491  cayleyhamilton  21498  1stcelcls  22069  imasdsf1olem  22983  comet  23123  nrmmetd  23184  tngngp  23263  tngngp3  23265  nmvs  23285  mulc1cncf  23513  cncfco  23515  pi1xfr  23659  pi1coghm  23665  caubl  23911  caublcls  23912  bcthlem2  23928  bcthlem3  23929  bcthlem4  23930  bcthlem5  23931  ivthlem2  24053  ovolicc2lem4  24121  volsuplem  24156  volsup  24157  uniioombllem3  24186  itg1climres  24315  itg2monolem1  24351  itg2i1fseqle  24355  itg2i1fseq  24356  itg2i1fseq2  24357  itg2addlem  24359  itgeq2  24378  dvferm1lem  24581  dvferm2lem  24583  dvlip  24590  c1lip1  24594  lhop1lem  24610  lhop1  24611  ftc1lem4  24636  ftc1lem6  24638  mdegmullem  24672  coe1mul3  24693  ply1divex  24730  coeeu  24815  coeeq  24817  coemullem  24840  coemul  24842  dvply1  24873  dvply2g  24874  aalioulem3  24923  aaliou3lem8  24934  ulmshftlem  24977  ulmshft  24978  ulmss  24985  pserdvlem2  25016  cxpcn3lem  25328  loglesqrt  25339  birthdaylem2  25530  emcllem2  25574  emcllem3  25575  harmonicbnd2  25582  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgambdd  25614  lgamcvglem  25617  facgam  25643  ftalem7  25656  bposlem7  25866  bposlem9  25868  lgsqrlem2  25923  lgsqrlem4  25925  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  rplogsumlem1  26060  dchrvmasumlem1  26071  logsqvma  26118  logsqvma2  26119  selberglem3  26123  selberg  26124  selberg2lem  26126  selberg4lem1  26136  pntrsumo1  26141  selberg34r  26147  pntsval  26148  pntsval2  26152  pntrlog2bndlem1  26153  pntrlog2bndlem4  26156  pntpbnd  26164  pntibnd  26169  pntlemo  26183  ewlkinedg  27386  wkslem1  27389  uspgr2wlkeq  27427  wlkdlem2  27465  upgrwlkdvdelem  27517  crctcshwlkn0lem2  27589  crctcshwlkn0lem3  27590  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  wlkiswwlks2lem2  27648  wlkiswwlks2lem5  27651  wwlksnext  27671  wwlksnredwwlkn  27673  wwlksnextproplem2  27689  clwwlkccatlem  27767  clwlkclwwlklem2a1  27770  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwwisshclwwslemlem  27791  clwwisshclwws  27793  clwwlknlbonbgr1  27817  clwwlkel  27825  clwwlkf  27826  clwwlkwwlksb  27833  clwwlkext2edg  27835  wwlksext2clwwlk  27836  clwwlknonex2lem2  27887  eupthseg  27985  upgreupthseg  27988  eupth2lem3  28015  2clwwlk2clwwlklem  28125  2clwwlk  28126  numclwwlk1lem2f1  28136  numclwlk1lem2  28149  nvs  28440  nvtri  28447  ipval  28480  blocnilem  28581  phpar2  28600  phpar  28601  sii  28631  normsub0  28913  norm-ii  28915  norm-iii  28917  normsub  28920  normpyth  28922  norm3dif  28927  norm3lemt  28929  norm3adifi  28930  normpar  28932  polid  28936  bcs  28958  pjaddi  29463  pjsubi  29465  pjmuli  29466  pjcjt2  29469  lnopeq0lem2  29783  lnopunilem2  29788  branmfn  29882  hstel2  29996  stj  30012  cdj3lem1  30211  cdj3lem2b  30214  cdj3lem3b  30217  cdj3i  30218  cnre2csqlem  31153  cnre2csqima  31154  mndpluscn  31169  lmdvg  31196  plymulx  31818  signsvfn  31852  subfacval2  32434  cvmliftlem7  32538  elmrsubrn  32767  faclim2  32980  fwddifval  33623  fwddifnval  33624  dnival  33810  unblimceq0lem  33845  unbdqndv2  33850  matunitlindf  34905  poimirlem32  34939  itg2gt0cn  34962  ftc1cnnclem  34980  ftc1cnnc  34981  areacirc  35002  sdclem1  35033  fdc  35035  seqpo  35037  incsequz  35038  incsequz2  35039  mettrifi  35047  caushft  35051  bfplem1  35115  ghomco  35184  rngohomadd  35262  rngohommul  35263  dihval  38383  lclkrlem1  38657  hdmap14lem2a  39018  hgmapval  39038  prjspnval  39315  incssnn0  39357  rencldnfilem  39466  irrapxlem5  39472  irrapxlem6  39473  pellexlem3  39477  cvgdvgrat  40694  radcnvrat  40695  hashnzfzclim  40703  binomcxplemradcnv  40733  iunincfi  41409  monoords  41613  fperiodmullem  41619  monoordxrv  41807  monoordxr  41808  monoord2xrv  41809  monoord2xr  41810  climinf  41936  climsuse  41938  climinff  41941  mullimc  41946  mullimcf  41953  idlimc  41956  limcperiod  41958  limcrecl  41959  limclner  41981  climinf2  42037  climxrrelem  42079  cnrefiisplem  42159  cnrefiisp  42160  climxlim2lem  42175  cncfshift  42206  cncfperiod  42211  fperdvper  42252  dvnmul  42277  iblspltprt  42307  itgspltprt  42313  itgiccshift  42314  itgperiod  42315  dirkerval2  42428  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkercncflem2  42438  dirkercncflem3  42439  fourierdlem29  42470  elaa2lem  42567  elaa2  42568  nnfoctbdj  42787  meaiuninclem  42811  meaiunincf  42814  meaiuninc3v  42815  meaiuninc3  42816  meaiininclem  42817  meaiininc  42818  smflimlem6  43101  smonoord  43580  iccpartimp  43626  iccelpart  43642  icceuelpart  43645  fargshiftfv  43648  fmtnorec2  43754  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbnd  44023  mgmhmlin  44102  rnghmmul  44220  c0snmgmhm  44234  zrrnghm  44237  ply1mulgsumlem3  44491  ply1mulgsumlem4  44492  ply1mulgsum  44493