Theorem fvoveq1 7391

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6500  (class class class)co 7368

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  coof  7656  fldiv4p1lem1div2  13767  fldiv4lem1div2  13769  modval  13803  seqval  13947  seqp1  13951  seqshft2  13963  monoord  13967  monoord2  13968  seqhomo  13984  facp1  14213  faclbnd4lem2  14229  bcval  14239  lsw0  14500  ccatval1  14512  ccatval2  14513  ccatalpha  14529  swrdfv  14584  2swrd2eqwrdeq  14888  imval  15042  recan  15272  rlimcld2  15513  rlimcn1  15523  rlimcn3  15525  climcn1  15527  climcn2  15528  subcn2  15530  o1of2  15548  isercoll2  15604  climsup  15605  serf0  15616  iseraltlem2  15618  fsumrelem  15742  mertenslem1  15819  mertenslem2  15820  mertens  15821  bitsfval  16362  smuval  16420  pcfac  16839  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  vdwlem10  16930  imasaddvallem  17462  imasvscafn  17470  imasvscaval  17471  chnltm1  18544  chnind  18556  mgmhmlin  18636  mhmlin  18730  mhmlem  19004  mulginvcom  19041  mhmmulg  19057  ghmlin  19162  efgsdm  19671  efgsdmi  19673  efgsrel  19675  efgsp1  19678  frgpup1  19716  rnghmmul  20397  c0snmgmhm  20410  zrrnghm  20481  abvmul  20766  abvtri  20767  issrngd  20800  lmhmlin  20999  ipcj  21601  psrmulval  21912  mhpmulcl  22104  psdcoef  22115  psdadd  22118  psdpw  22125  coe1mul2  22223  coe1tmmul2fv  22232  coe1pwmulfv  22234  cply1mul  22252  mat1scmat  22495  mdetmul  22579  madufval  22593  cramer0  22646  cpmatmcllem  22674  d1mat2pmat  22695  m2cpminvid2lem  22710  decpmatmullem  22727  decpmatmulsumfsupp  22729  pm2mpmhmlem1  22774  pm2mpmhmlem2  22775  cayhamlem1  22822  cpmadumatpoly  22839  cayleyhamilton  22846  1stcelcls  23417  imasdsf1olem  24329  comet  24469  nrmmetd  24530  tngngp  24610  tngngp3  24612  nmvs  24632  mulc1cncf  24866  cncfco  24868  pi1xfr  25023  pi1coghm  25029  caubl  25276  caublcls  25277  bcthlem2  25293  bcthlem3  25294  bcthlem4  25295  bcthlem5  25296  ivthlem2  25421  ovolicc2lem4  25489  volsuplem  25524  volsup  25525  uniioombllem3  25554  itg1climres  25683  itg2monolem1  25719  itg2i1fseqle  25723  itg2i1fseq  25724  itg2i1fseq2  25725  itg2addlem  25727  itgeq2  25747  dvferm1lem  25956  dvferm2lem  25958  dvlip  25966  c1lip1  25970  lhop1lem  25986  lhop1  25987  ftc1lem4  26014  ftc1lem6  26016  mdegmullem  26051  coe1mul3  26072  ply1divex  26110  coeeu  26198  coeeq  26200  coemullem  26223  coemul  26225  dvply1  26259  dvply2g  26260  dvply2gOLD  26261  aalioulem3  26310  aaliou3lem8  26321  ulmshftlem  26366  ulmshft  26367  ulmss  26374  pserdvlem2  26406  cxpcn3lem  26725  loglesqrt  26739  birthdaylem2  26930  emcllem2  26975  emcllem3  26976  harmonicbnd2  26983  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem5  27011  lgambdd  27015  lgamcvglem  27018  facgam  27044  ftalem7  27057  bposlem7  27269  bposlem9  27271  lgsqrlem2  27326  lgsqrlem4  27328  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  rplogsumlem1  27463  dchrvmasumlem1  27474  logsqvma  27521  logsqvma2  27522  selberglem3  27526  selberg  27527  selberg2lem  27529  selberg4lem1  27539  pntrsumo1  27544  selberg34r  27550  pntsval  27551  pntsval2  27555  pntrlog2bndlem1  27556  pntrlog2bndlem4  27559  pntpbnd  27567  pntibnd  27572  pntlemo  27586  addbday  28026  addonbday  28287  seqsval  28296  seqsp1  28319  bdaypw2n0bndlem  28471  ewlkinedg  29690  wkslem1  29693  uspgr2wlkeq  29731  wlkdlem2  29767  upgrwlkdvdelem  29821  crctcshwlkn0lem2  29896  crctcshwlkn0lem3  29897  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  wlkiswwlks2lem2  29955  wlkiswwlks2lem5  29958  wwlksnext  29978  wwlksnredwwlkn  29980  wwlksnextproplem2  29995  clwwlkccatlem  30076  clwlkclwwlklem2a1  30079  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwwisshclwwslemlem  30100  clwwisshclwws  30102  clwwlknlbonbgr1  30126  clwwlkel  30133  clwwlkf  30134  clwwlkwwlksb  30141  clwwlkext2edg  30143  wwlksext2clwwlk  30144  clwwlknonex2lem2  30195  eupthseg  30293  upgreupthseg  30296  eupth2lem3  30323  2clwwlk2clwwlklem  30433  2clwwlk  30434  numclwwlk1lem2f1  30444  numclwlk1lem2  30457  nvs  30751  nvtri  30758  ipval  30791  blocnilem  30892  phpar2  30911  phpar  30912  sii  30942  normsub0  31224  norm-ii  31226  norm-iii  31228  normsub  31231  normpyth  31233  norm3dif  31238  norm3lemt  31240  norm3adifi  31241  normpar  31243  polid  31247  bcs  31269  pjaddi  31774  pjsubi  31776  pjmuli  31777  pjcjt2  31780  lnopeq0lem2  32094  lnopunilem2  32099  branmfn  32193  hstel2  32307  stj  32323  cdj3lem1  32522  cdj3lem2b  32525  cdj3lem3b  32528  cdj3i  32529  ccatws1f1o  33044  gsummulsubdishift1  33162  elrgspnlem2  33337  constrsuc  33916  cnre2csqlem  34088  cnre2csqima  34089  mndpluscn  34104  lmdvg  34131  plymulx  34726  signsvfn  34760  subfacval2  35403  cvmliftlem7  35507  elmrsubrn  35736  faclim2  35964  fwddifval  36378  fwddifnval  36379  dnival  36693  unblimceq0lem  36728  unbdqndv2  36733  matunitlindf  37869  poimirlem32  37903  itg2gt0cn  37926  ftc1cnnclem  37942  ftc1cnnc  37943  areacirc  37964  sdclem1  37994  fdc  37996  seqpo  37998  incsequz  37999  incsequz2  38000  mettrifi  38008  caushft  38012  bfplem1  38073  ghomco  38142  rngohomadd  38220  rngohommul  38221  dihval  41608  lclkrlem1  41882  hdmap14lem2a  42243  hgmapval  42263  deg1pow  42511  sticksstones10  42525  sticksstones12a  42527  abvexp  42902  fsuppind  42948  prjspnval  42974  incssnn0  43068  rencldnfilem  43177  irrapxlem5  43183  irrapxlem6  43184  pellexlem3  43188  cvgdvgrat  44669  radcnvrat  44670  hashnzfzclim  44678  binomcxplemradcnv  44708  iunincfi  45453  monoords  45659  fperiodmullem  45665  monoordxrv  45839  monoordxr  45840  monoord2xrv  45841  monoord2xr  45842  climinf  45966  climsuse  45968  climinff  45971  mullimc  45976  mullimcf  45983  idlimc  45986  limcperiod  45988  limcrecl  45989  limclner  46009  climinf2  46065  climxrrelem  46107  cnrefiisplem  46187  cnrefiisp  46188  climxlim2lem  46203  cncfshift  46232  cncfperiod  46237  fperdvper  46277  dvnmul  46301  iblspltprt  46331  itgspltprt  46337  itgiccshift  46338  itgperiod  46339  dirkerval2  46452  dirkertrigeqlem1  46456  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkercncflem2  46462  dirkercncflem3  46463  fourierdlem29  46494  elaa2lem  46591  elaa2  46592  nnfoctbdj  46814  meaiuninclem  46838  meaiunincf  46841  meaiuninc3v  46842  meaiuninc3  46843  meaiininclem  46844  meaiininc  46845  smflimlem6  47134  ormkglobd  47233  natglobalincr  47235  2ltceilhalf  47688  ceilhalfnn  47696  smonoord  47731  iccpartimp  47777  iccelpart  47793  icceuelpart  47796  fargshiftfv  47799  fmtnorec2  47903  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbnd  48169  upgrimwlklem5  48261  gpgov  48402  gpg5nbgrvtx13starlem2  48432  ply1mulgsumlem3  48748  ply1mulgsumlem4  48749  ply1mulgsum  48750  ackvalsuc1  49039