Theorem fvoveq1 7432

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

Syntax hints:   → wi 4   = wceq 1542  ‘cfv 6544  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  eluzaddOLD  12857  eluzsubOLD  12858  fldiv4p1lem1div2  13800  fldiv4lem1div2  13802  modval  13836  seqval  13977  seqp1  13981  seqshft2  13994  monoord  13998  monoord2  13999  seqhomo  14015  facp1  14238  faclbnd4lem2  14254  bcval  14264  lsw0  14515  ccatval1  14527  ccatval2  14528  ccatalpha  14543  swrdfv  14598  2swrd2eqwrdeq  14904  imval  15054  recan  15283  rlimcld2  15522  rlimcn1  15532  rlimcn3  15534  climcn1  15536  climcn2  15537  subcn2  15539  o1of2  15557  isercoll2  15615  climsup  15616  serf0  15627  iseraltlem2  15629  fsumrelem  15753  mertenslem1  15830  mertenslem2  15831  mertens  15832  bitsfval  16364  smuval  16422  pcfac  16832  vdwlem6  16919  vdwlem8  16921  vdwlem9  16922  vdwlem10  16923  imasaddvallem  17475  imasvscafn  17483  imasvscaval  17484  mhmlin  18679  mhmlem  18945  mulginvcom  18979  mhmmulg  18995  ghmlin  19097  efgsdm  19598  efgsdmi  19600  efgsrel  19602  efgsp1  19605  frgpup1  19643  abvmul  20437  abvtri  20438  issrngd  20469  lmhmlin  20646  ipcj  21187  psrmulval  21505  mhpmulcl  21692  coe1mul2  21791  coe1tmmul2fv  21800  coe1pwmulfv  21802  cply1mul  21818  mat1scmat  22041  mdetmul  22125  madufval  22139  cramer0  22192  cpmatmcllem  22220  d1mat2pmat  22241  m2cpminvid2lem  22256  decpmatmullem  22273  decpmatmulsumfsupp  22275  pm2mpmhmlem1  22320  pm2mpmhmlem2  22321  cayhamlem1  22368  cpmadumatpoly  22385  cayleyhamilton  22392  1stcelcls  22965  imasdsf1olem  23879  comet  24022  nrmmetd  24083  tngngp  24171  tngngp3  24173  nmvs  24193  mulc1cncf  24421  cncfco  24423  pi1xfr  24571  pi1coghm  24577  caubl  24825  caublcls  24826  bcthlem2  24842  bcthlem3  24843  bcthlem4  24844  bcthlem5  24845  ivthlem2  24969  ovolicc2lem4  25037  volsuplem  25072  volsup  25073  uniioombllem3  25102  itg1climres  25232  itg2monolem1  25268  itg2i1fseqle  25272  itg2i1fseq  25273  itg2i1fseq2  25274  itg2addlem  25276  itgeq2  25295  dvferm1lem  25501  dvferm2lem  25503  dvlip  25510  c1lip1  25514  lhop1lem  25530  lhop1  25531  ftc1lem4  25556  ftc1lem6  25558  mdegmullem  25596  coe1mul3  25617  ply1divex  25654  coeeu  25739  coeeq  25741  coemullem  25764  coemul  25766  dvply1  25797  dvply2g  25798  aalioulem3  25847  aaliou3lem8  25858  ulmshftlem  25901  ulmshft  25902  ulmss  25909  pserdvlem2  25940  cxpcn3lem  26255  loglesqrt  26266  birthdaylem2  26457  emcllem2  26501  emcllem3  26502  harmonicbnd2  26509  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem5  26537  lgambdd  26541  lgamcvglem  26544  facgam  26570  ftalem7  26583  bposlem7  26793  bposlem9  26795  lgsqrlem2  26850  lgsqrlem4  26852  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  rplogsumlem1  26987  dchrvmasumlem1  26998  logsqvma  27045  logsqvma2  27046  selberglem3  27050  selberg  27051  selberg2lem  27053  selberg4lem1  27063  pntrsumo1  27068  selberg34r  27074  pntsval  27075  pntsval2  27079  pntrlog2bndlem1  27080  pntrlog2bndlem4  27083  pntpbnd  27091  pntibnd  27096  pntlemo  27110  ewlkinedg  28861  wkslem1  28864  uspgr2wlkeq  28903  wlkdlem2  28940  upgrwlkdvdelem  28993  crctcshwlkn0lem2  29065  crctcshwlkn0lem3  29066  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  wlkiswwlks2lem2  29124  wlkiswwlks2lem5  29127  wwlksnext  29147  wwlksnredwwlkn  29149  wwlksnextproplem2  29164  clwwlkccatlem  29242  clwlkclwwlklem2a1  29245  clwlkclwwlklem2fv1  29248  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwwisshclwwslemlem  29266  clwwisshclwws  29268  clwwlknlbonbgr1  29292  clwwlkel  29299  clwwlkf  29300  clwwlkwwlksb  29307  clwwlkext2edg  29309  wwlksext2clwwlk  29310  clwwlknonex2lem2  29361  eupthseg  29459  upgreupthseg  29462  eupth2lem3  29489  2clwwlk2clwwlklem  29599  2clwwlk  29600  numclwwlk1lem2f1  29610  numclwlk1lem2  29623  nvs  29916  nvtri  29923  ipval  29956  blocnilem  30057  phpar2  30076  phpar  30077  sii  30107  normsub0  30389  norm-ii  30391  norm-iii  30393  normsub  30396  normpyth  30398  norm3dif  30403  norm3lemt  30405  norm3adifi  30406  normpar  30408  polid  30412  bcs  30434  pjaddi  30939  pjsubi  30941  pjmuli  30942  pjcjt2  30945  lnopeq0lem2  31259  lnopunilem2  31264  branmfn  31358  hstel2  31472  stj  31488  cdj3lem1  31687  cdj3lem2b  31690  cdj3lem3b  31693  cdj3i  31694  cnre2csqlem  32890  cnre2csqima  32891  mndpluscn  32906  lmdvg  32933  plymulx  33559  signsvfn  33593  subfacval2  34178  cvmliftlem7  34282  elmrsubrn  34511  faclim2  34718  fwddifval  35134  fwddifnval  35135  dnival  35347  unblimceq0lem  35382  unbdqndv2  35387  matunitlindf  36486  poimirlem32  36520  itg2gt0cn  36543  ftc1cnnclem  36559  ftc1cnnc  36560  areacirc  36581  sdclem1  36611  fdc  36613  seqpo  36615  incsequz  36616  incsequz2  36617  mettrifi  36625  caushft  36629  bfplem1  36690  ghomco  36759  rngohomadd  36837  rngohommul  36838  dihval  40103  lclkrlem1  40377  hdmap14lem2a  40738  hgmapval  40758  sticksstones10  40971  sticksstones12a  40973  fsuppind  41162  prjspnval  41358  incssnn0  41449  rencldnfilem  41558  irrapxlem5  41564  irrapxlem6  41565  pellexlem3  41569  cvgdvgrat  43072  radcnvrat  43073  hashnzfzclim  43081  binomcxplemradcnv  43111  iunincfi  43783  monoords  44007  fperiodmullem  44013  monoordxrv  44192  monoordxr  44193  monoord2xrv  44194  monoord2xr  44195  climinf  44322  climsuse  44324  climinff  44327  mullimc  44332  mullimcf  44339  idlimc  44342  limcperiod  44344  limcrecl  44345  limclner  44367  climinf2  44423  climxrrelem  44465  cnrefiisplem  44545  cnrefiisp  44546  climxlim2lem  44561  cncfshift  44590  cncfperiod  44595  fperdvper  44635  dvnmul  44659  iblspltprt  44689  itgspltprt  44695  itgiccshift  44696  itgperiod  44697  dirkerval2  44810  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkercncflem2  44820  dirkercncflem3  44821  fourierdlem29  44852  elaa2lem  44949  elaa2  44950  nnfoctbdj  45172  meaiuninclem  45196  meaiunincf  45199  meaiuninc3v  45200  meaiuninc3  45201  meaiininclem  45202  meaiininc  45203  smflimlem6  45492  natglobalincr  45591  tworepnotupword  45600  smonoord  46039  iccpartimp  46085  iccelpart  46101  icceuelpart  46104  fargshiftfv  46107  fmtnorec2  46211  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbnd  46477  mgmhmlin  46556  rnghmmul  46698  c0snmgmhm  46713  zrrnghm  46716  ply1mulgsumlem3  47069  ply1mulgsumlem4  47070  ply1mulgsum  47071  ackvalsuc1  47365