Theorem fveqeq2 6841

Description: Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)

Assertion

Ref	Expression
fveqeq2	⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Proof of Theorem fveqeq2

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fveqeq2d 6840	1 ⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ‘cfv 6490

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498

This theorem is referenced by:  fvelimad  6899  dff13f  7199  f1veqaeq  7200  f1elima  7207  fpropnf1  7211  nf1const  7248  oteqimp  7950  fimaproj  8075  suppfnss  8129  suppssfv  8142  tz7.48lem  8370  seqomlem1  8379  seqomlem2  8380  fofinf1o  9230  fipreima  9256  cantnfp1lem3  9587  brttrcl2  9621  ssttrcl  9622  ttrcltr  9623  tcrank  9794  updjudhcoinlf  9842  updjudhcoinrg  9843  pm54.43lem  9910  ackbij1lem18  10144  ackbij1  10145  axcc2  10345  iunfo  10447  grur1  10729  injresinjlem  13704  injresinj  13705  suppssfz  13915  seqid2  13969  hashrabsn01  14294  hashrabsn1  14295  hashimarni  14362  hashbclem  14373  hashbc  14374  hash2exprb  14392  elss2prb  14409  hash2sspr  14410  hash3tpde  14414  fi1uzind  14428  brfi1indALT  14431  wrdmap  14467  wrdl1s1  14536  wrdind  14643  wrd2ind  14644  reuccatpfxs1lem  14667  reuccatpfxs1  14668  cshf1  14731  cshw1  14743  wwlktovf  14877  wwlktovf1  14878  wwlktovfo  14879  wrd2f1tovbij  14881  wrdl3s3  14883  abs1m  15257  sumrblem  15632  fsumcvg  15633  summolem2a  15636  incexc2  15759  ntrivcvgfvn0  15820  prodrblem  15850  fprodcvg  15851  prodmolem2a  15855  smupvallem  16408  smu01lem  16410  algfx  16505  iserodd  16761  prmreclem2  16843  prmreclem3  16844  vdwlem2  16908  vdwlem6  16912  vdwlem8  16914  hashbcval  16928  ramub1lem1  16952  ramub1lem2  16953  imasleval  17460  eldmcoa  17987  coaval  17990  ghmf1  19173  ghmqusnsglem1  19207  ghmquskerlem1  19210  orbsta  19240  symgextf1  19348  psgnunilem2  19422  psgnunilem3  19423  psgnunilem4  19424  odeq1  19487  odngen  19504  sylow1lem2  19526  sylow1lem4  19528  sylow1lem5  19529  pgpfi  19532  efgtlen  19653  efgsfo  19666  efgredlemd  19671  efgred  19675  gsummptnn0fzfv  19914  isabvd  20743  abveq0  20749  abvdom  20761  islbs  21026  isobs  21673  cply1mul  22238  mdetunilem1  22554  mdetunilem4  22557  mdetunilem8  22561  mdetunilem9  22562  pmatcoe1fsupp  22643  m2cpminvid2lem  22696  mp2pm2mplem4  22751  2ndci  23390  2ndcsb  23391  2ndcsep  23401  txkgen  23594  nmoeq0  24678  nmoleub3  25073  ivth  25409  ivthle  25411  ivthle2  25412  ovolunlem1  25452  ovolicc2  25477  volivth  25562  mbfinf  25620  itg2splitlem  25703  rollelem  25947  rolle  25948  tdeglem4  26019  mdeglt  26024  deg1leb  26054  deg1lt  26056  fta1g  26129  ig1peu  26134  ig1pval3  26137  dgrle  26202  0dgrb  26205  dgreq0  26225  fta1lem  26269  fta1  26270  aannenlem1  26290  aannenlem2  26291  aalioulem2  26295  reeff1o  26411  eflogeq  26565  argregt0  26573  argrege0  26574  efopn  26621  asinsinb  26861  acoscosb  26862  atantanb  26888  musum  27155  dchrptlem1  27229  dchrptlem2  27230  lgsquadlem1  27345  nosupcbv  27668  nosupfv  27672  noinfcbv  27683  noinffv  27687  nocvxmin  27745  scutbday  27772  eqscut  27773  scutun12  27778  scutbdaylt  27786  cuteq0  27803  negsleft  28027  negsright  28028  onsiso  28236  bdayn0sf1o  28328  dfnns2  28330  znegscl  28350  renegscl  28443  istrkgl  28479  mirreu  28685  israg  28718  lmireu  28811  lmieq  28812  gropd  29053  grstructd  29054  umgredg2  29122  umgrbi  29123  umgrnloopv  29128  umgredgprv  29129  edgumgr  29157  numedglnl  29166  umgredgnlp  29169  edgusgr  29182  usgruspgrb  29205  uhgr2edg  29230  usgredg2v  29249  ushgredgedgloop  29253  usgr1e  29267  usgrexmplef  29281  subumgredg2  29307  umgrreslem  29327  cusgrexilem2  29464  cusgrexg  29466  fusgrn0degnn0  29522  umgr2v2e  29548  vdiscusgr  29554  rusgr1vtxlem  29610  rgrusgrprc  29612  wlkon2n0  29687  upgrwlkdvdelem  29758  spthonepeq  29774  usgr2wlkneq  29778  iswwlksn  29860  wwlksnon  29873  wwlksn0  29885  wlkiswwlksupgr2  29899  wlknwwlksnbij  29910  wwlksnextbi  29916  wwlksnextfun  29920  wwlksnextinj  29921  wwlksnextbij  29924  2pthon3v  29965  umgr2wlk  29971  rusgrnumwwlkb0  29996  isclwwlkn  30051  clwwlkn1loopb  30067  hashecclwwlkn1  30101  s2elclwwlknon2  30128  uhgr3cyclex  30206  frgrwopreglem4a  30334  frgrwopreglem3  30338  frgrwopreglem5lem  30344  frgrwopreglem5  30345  frgrregorufr0  30348  friendshipgt3  30422  nvz  30693  nmlno0i  30818  norm1exi  31274  pjoc1  31458  pjoc2  31463  pj11  31738  elnlfn  31952  nmlnop0  32022  adjbd1o  32109  strlem1  32274  stcltr1i  32298  2ndimaxp  32673  fnpreimac  32698  indf1ofs  32897  isarchi  33213  ply1dg1rt  33610  extvfval  33646  esplyfval0  33671  esplymhp  33675  esplyfv1  33676  vieta  33685  minplyval  33811  qtophaus  33942  locfinreflem  33946  rhmpreimacn  33991  isrrext  34106  eulerpartlemsv3  34467  eulerpartlemgvv  34482  ballotlemelo  34594  ballotlemfmpn  34601  ballotlemiex  34608  ballotlemi1  34609  ballotlemii  34610  ballotlemfrcn0  34636  ballotlemirc  34638  bnj229  34989  bnj517  34990  bnj590  35015  bnj1097  35086  bnj1118  35089  bnj1128  35095  bnj1145  35098  f1resfz0f1d  35257  loop1cycl  35280  umgr2cycl  35284  subfacp1lem3  35325  cvmlift3lem5  35466  satffunlem1lem1  35545  satffunlem2lem1  35547  satffunlem2lem2  35549  mthmi  35720  rankeq1o  36314  weiunfr  36610  finxpreclem6  37540  poimirlem13  37773  poimirlem14  37774  poimirlem17  37777  poimirlem18  37778  poimirlem21  37781  poimirlem27  37787  poimirlem28  37788  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  lfl1  39269  lshpkrex  39317  cdleme50rnlem  40743  dochkr1  41677  dochkr1OLDN  41678  lcfrlem28  41769  mapd1o  41847  hdmap1vallem  41996  aks6d1c4  42317  hashnexinjle  42322  sticksstones2  42340  sticksstones3  42341  aks6d1c6lem3  42365  aks6d1c6isolem1  42367  aks6d1c6isolem2  42368  grpods  42387  unitscyglem1  42388  unitscyglem2  42389  unitscyglem3  42390  unitscyglem4  42391  unitscyglem5  42392  diophrw  42943  eldioph3  42950  diophin  42956  eq0rabdioph  42960  eldioph4b  42995  fphpdo  43001  fnwe2lem2  43235  fnwe2lem3  43236  islssfgi  43256  hbt  43314  dgraaval  43328  dgraalem  43329  dgraaub  43332  mpaaeu  43334  mpaaval  43335  mpaalem  43336  rngunsnply  43353  idomsubgmo  43377  proot1mul  43378  cantnfresb  43508  fvelrnbf  45205  wessf1ornlem  45371  sumnnodd  45818  fourierdlem2  46295  fourierdlem3  46296  fcoresf1  47257  uniimafveqt  47569  elsetpreimafvrab  47582  prpair  47689  prproropf1olem1  47691  pairreueq  47698  paireqne  47699  prprspr2  47706  reuprpr  47711  requad2  47811  cycldlenngric  48116  uhgrimisgrgriclem  48118  clnbgrgrimlem  48121  clnbgrgrim  48122  usgrgrtrirex  48138  stgrusgra  48147  uspgrlimlem1  48176  uspgrlimlem2  48177  grlimgrtri  48191  usgrexmpl1lem  48209  usgrexmpl2lem  48214  gpgusgralem  48244  gpgprismgr4cyclex  48295  uspgrsprfo  48336  ply1mulgsumlem2  48575  lindslinindsimp1  48645  snlindsntor  48659  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  nn0sumshdiglem1  48809  nn0sumshdig  48811  istermc  49661