Theorem fvoveq1 7437

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

Assertion

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

Proof of Theorem fvoveq1

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ‘cfv 6533  (class class class)co 7414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417

This theorem is used by:  coof  7703  fldiv4p1lem1div2  13899  fldiv4lem1div2  13901  modval  13935  seqval  14079  seqp1  14083  seqshft2  14095  monoord  14099  monoord2  14100  seqhomo  14116  facp1  14345  faclbnd4lem2  14361  bcval  14371  lsw0  14633  ccatval1  14645  ccatval2  14646  ccatalpha  14663  swrdfv  14719  2swrd2eqwrdeq  15029  imval  15197  recan  15427  rlimcld2  15668  rlimcn1  15678  rlimcn3  15680  climcn1  15682  climcn2  15683  subcn2  15685  o1of2  15703  isercoll2  15759  climsup  15760  serf0  15771  iseraltlem2  15773  fsumrelem  15897  mertenslem1  15976  mertenslem2  15977  mertens  15978  bitsfval  16516  smuval  16574  pcfac  16994  vdwlem6  17081  vdwlem8  17083  vdwlem9  17084  vdwlem10  17085  imasaddvallem  17618  imasvscafn  17626  imasvscaval  17627  chnltm1  18700  chnind  18712  mgmhmlin  18804  mhmlin  18904  mhmlem  19188  mulginvcom  19225  mhmmulg  19241  ghmlin  19351  efgsdm  19860  efgsdmi  19862  efgsrel  19864  efgsp1  19867  frgpup1  19905  rnghmmul  20593  c0snmgmhm  20606  zrrnghm  20701  abvmul  20990  abvtri  20991  issrngd  21024  lmhmlin  21222  ipcj  21850  psrmulval  22162  mhpmulcl  22380  psdcoef  22391  psdadd  22394  psdpw  22401  coe1mul2  22498  coe1tmmul2fv  22507  coe1pwmulfv  22509  cply1mul  22524  mat1scmat  22764  mdetmul  22848  madufval  22862  matunitlindf  22906  cramer0  22918  cpmatmcllem  22946  d1mat2pmat  22967  m2cpminvid2lem  22982  decpmatmullem  22999  decpmatmulsumfsupp  23001  pm2mpmhmlem1  23046  pm2mpmhmlem2  23047  cayhamlem1  23094  cpmadumatpoly  23111  cayleyhamilton  23118  1stcelcls  23690  imasdsf1olem  24602  comet  24742  nrmmetd  24803  tngngp  24883  tngngp3  24885  nmvs  24905  mulc1cncf  25136  cncfco  25138  pi1xfr  25286  pi1coghm  25292  caubl  25539  caublcls  25540  bcthlem2  25556  bcthlem3  25557  bcthlem4  25558  bcthlem5  25559  ivthlem2  25683  ovolicc2lem4  25751  volsuplem  25786  volsup  25787  uniioombllem3  25816  itg1climres  25945  itg2monolem1  25981  itg2i1fseqle  25985  itg2i1fseq  25986  itg2i1fseq2  25987  itg2addlem  25989  itgeq2  26008  dvferm1lem  26214  dvferm2lem  26216  dvlip  26223  c1lip1  26227  lhop1lem  26243  lhop1  26244  ftc1lem4  26269  ftc1lem6  26271  mdegmullem  26306  coe1mul3  26327  ply1divex  26365  coeeu  26454  coeeq  26456  coemullem  26479  coemul  26481  plymulidp  26515  dvply1  26517  dvply2g  26518  aalioulem3  26573  aaliou3lem8  26584  ulmshftlem  26628  ulmshft  26629  ulmss  26636  pserdvlem2  26667  cxpcn3lem  26987  loglesqrt  27001  birthdaylem2  27192  emcllem2  27236  emcllem3  27237  harmonicbnd2  27244  lgamgulmlem2  27269  lgamgulmlem3  27270  lgamgulmlem5  27272  lgambdd  27276  lgamcvglem  27279  facgam  27305  ftalem7  27318  bposlem7  27529  bposlem9  27531  lgsqrlem2  27586  lgsqrlem4  27588  2lgslem3a  27635  2lgslem3b  27636  2lgslem3c  27637  2lgslem3d  27638  rplogsumlem1  27723  dchrvmasumlem1  27734  logsqvma  27781  logsqvma2  27782  selberglem3  27786  selberg  27787  selberg2lem  27789  selberg4lem1  27799  pntrsumo1  27804  selberg34r  27810  pntsval  27811  pntsval2  27815  pntrlog2bndlem1  27816  pntrlog2bndlem4  27819  pntpbnd  27827  pntibnd  27832  pntlemo  27846  addbday  28286  addonbday  28547  seqsval  28556  seqsp1  28579  bdaypw2n0bndlem  28731  ewlkinedg  30067  wkslem1  30070  uspgr2wlkeq  30108  wlkdlem2  30144  upgrwlkdvdelem  30204  crctcshwlkn0lem2  30282  crctcshwlkn0lem3  30283  crctcshwlkn0lem4  30284  crctcshwlkn0lem5  30285  wlkiswwlks2lem2  30341  wlkiswwlks2lem5  30344  wwlksnext  30364  wwlksnredwwlkn  30366  wwlksnextproplem2  30381  clwwlkccatlem  30462  clwlkclwwlklem2a1  30465  clwlkclwwlklem2fv1  30468  clwlkclwwlklem2a4  30470  clwlkclwwlklem2a  30471  clwlkclwwlklem2  30473  clwwisshclwwslemlem  30486  clwwisshclwws  30488  clwwlknlbonbgr1  30512  clwwlkel  30519  clwwlkf  30520  clwwlkwwlksb  30527  clwwlkext2edg  30529  wwlksext2clwwlk  30530  clwwlknonex2lem2  30581  eupthseg  30689  upgreupthseg  30692  eupth2lem3  30719  2clwwlk2clwwlklem  30829  2clwwlk  30830  numclwwlk1lem2f1  30840  numclwlk1lem2  30853  nvs  31147  nvtri  31154  ipval  31187  blocnilem  31288  phpar2  31307  phpar  31308  sii  31338  normsub0  31620  norm-ii  31622  norm-iii  31624  normsub  31627  normpyth  31629  norm3dif  31634  norm3lemt  31636  norm3adifi  31637  normpar  31639  polid  31643  bcs  31665  pjaddi  32170  pjsubi  32172  pjmuli  32173  pjcjt2  32176  lnopeq0lem2  32490  lnopunilem2  32495  branmfn  32589  hstel2  32703  stj  32719  cdj3lem1  32918  cdj3lem2b  32921  cdj3lem3b  32924  cdj3i  32925  ccatws1f1o  33396  gsummulsubdishift1  33511  elrgspnlem2  33686  selvply1rhmlemb  34032  constrsuc  34251  cnre2csqlem  34423  cnre2csqima  34424  mndpluscn  34439  lmdvg  34466  signsvfn  35093  subfacval2  35769  cvmliftlem7  35873  elmrsubrn  36102  faclim2  36330  fwddifval  36745  fwddifnval  36746  dnival  37171  unblimceq0lem  37206  unbdqndv2  37211  poimirlem32  38404  itg2gt0cn  38427  ftc1cnnclem  38443  ftc1cnnc  38444  areacirc  38465  sdclem1  38496  fdc  38498  seqpo  38500  incsequz  38501  incsequz2  38502  mettrifi  38510  caushft  38514  bfplem1  38575  ghomco  38644  rngohomadd  38722  rngohommul  38723  dihval  42108  lclkrlem1  42382  hdmap14lem2a  42743  hgmapval  42763  deg1pow  43010  sticksstones10  43024  sticksstones12a  43026  abvexp  43417  fsuppind  43439  prjspnval  43465  incssnn0  43559  rencldnfilem  43664  irrapxlem5  43670  irrapxlem6  43671  pellexlem3  43675  cvgdvgrat  45140  radcnvrat  45141  hashnzfzclim  45149  binomcxplemradcnv  45179  iunincfi  45929  monoords  46133  fperiodmullem  46139  monoordxrv  46312  monoordxr  46313  monoord2xrv  46314  monoord2xr  46315  climinf  46439  climsuse  46441  climinff  46444  mullimc  46449  mullimcf  46456  idlimc  46459  limcperiod  46461  limcrecl  46462  limclner  46482  climinf2  46538  climxrrelem  46580  cnrefiisplem  46660  cnrefiisp  46661  climxlim2lem  46676  cncfshift  46705  cncfperiod  46710  fperdvper  46750  dvnmul  46774  iblspltprt  46804  itgspltprt  46810  itgiccshift  46811  itgperiod  46812  dirkerval2  46925  dirkertrigeqlem1  46929  dirkertrigeqlem2  46930  dirkertrigeqlem3  46931  dirkercncflem2  46935  dirkercncflem3  46936  fourierdlem29  46967  fourierdlem48  46985  fourierdlem49  46986  fourierdlem113  47050  elaa2lem  47064  elaa2  47065  nnfoctbdj  47287  meaiuninclem  47311  meaiunincf  47314  meaiuninc3v  47315  meaiuninc3  47316  meaiininclem  47317  meaiininc  47318  smflimlem6  47607  ormkglobd  47708  2ltceilhalf  48223  ceilhalfnn  48231  smonoord  48268  iccpartimp  48320  iccelpart  48336  icceuelpart  48339  fargshiftfv  48342  fmtnorec2  48449  ppivalnnnprmge6  48532  ppivalnnnprm  48534  ppivalnn  48538  bgoldbtbndlem2  48725  bgoldbtbndlem3  48726  bgoldbtbnd  48728  upgrimwlklem5  48820  gpgov  48961  gpg5nbgrvtx13starlem2  48991  ply1mulgsumlem3  49321  ply1mulgsumlem4  49322  ply1mulgsum  49323  ackvalsuc1  49612