Theorem fveqeq2 6894

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fveqeq2d 6893	1 ⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ‘cfv 6540

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548

This theorem is used by:  fvelimad  6952  dff13f  7258  f1veqaeq  7259  f1elima  7266  fpropnf1  7270  nf1const  7311  oteqimp  8011  fimaproj  8137  suppfnss  8191  suppssfv  8204  tz7.48lem  8434  seqomlem1  8443  seqomlem2  8444  fofinf1o  9296  fipreima  9322  cantnfp1lem3  9656  brttrcl2  9690  ssttrcl  9691  ttrcltr  9692  tcrank  9863  updjudhcoinlf  9934  updjudhcoinrg  9935  pm54.43lem  10002  ackbij1lem18  10235  ackbij1  10236  axcc2  10436  iunfo  10542  grur1  10824  injresinjlem  13840  injresinj  13841  f1resfz0f1d  13842  suppssfz  14052  seqid2  14106  hashrabsn01  14431  hashrabsn1  14432  hashimarni  14500  hashbclem  14511  hashbc  14512  hash2exprb  14530  elss2prb  14547  hash2sspr  14548  hash3tpde  14552  fi1uzind  14566  brfi1indALT  14569  wrdmap  14605  wrdl1s1  14676  wrdind  14785  wrd2ind  14786  reuccatpfxs1lem  14809  reuccatpfxs1  14810  cshf1  14875  cshw1  14887  wwlktovf  15021  wwlktovf1  15022  wwlktovfo  15023  wrd2f1tovbij  15025  wrdl3s3  15027  abs1m  15415  sumrblem  15789  fsumcvg  15790  summolem2a  15793  incexc2  15919  ntrivcvgfvn0  15980  prodrblem  16010  fprodcvg  16011  prodmolem2a  16015  smupvallem  16567  smu01lem  16569  algfx  16664  iserodd  16921  prmreclem2  17003  prmreclem3  17004  vdwlem2  17068  vdwlem6  17072  vdwlem8  17074  hashbcval  17088  ramub1lem1  17112  ramub1lem2  17113  imasleval  17621  eldmcoa  18148  coaval  18151  ghmf1  19364  ghmqusnsglem1  19398  ghmquskerlem1  19401  orbsta  19431  symgextf1  19539  psgnunilem2  19613  psgnunilem3  19614  psgnunilem4  19615  odeq1  19678  odngen  19695  sylow1lem2  19717  sylow1lem4  19719  sylow1lem5  19720  pgpfi  19723  efgtlen  19844  efgsfo  19857  efgredlemd  19862  efgred  19866  gsummptnn0fzfv  20105  isabvd  20969  abveq0  20975  abvdom  20987  islbs  21251  isobs  21924  cply1mul  22510  mdetunilem1  22823  mdetunilem4  22826  mdetunilem8  22830  mdetunilem9  22831  pmatcoe1fsupp  22912  m2cpminvid2lem  22965  mp2pm2mplem4  23020  2ndci  23659  2ndcsb  23660  2ndcsep  23671  txkgen  23864  nmoeq0  24948  nmoleub3  25333  ivth  25668  ivthle  25670  ivthle2  25671  ovolunlem1  25711  ovolicc2  25736  volivth  25821  mbfinf  25879  itg2splitlem  25962  rollelem  26203  rolle  26204  tdeglem4  26272  mdeglt  26277  deg1leb  26307  deg1lt  26309  fta1g  26382  ig1peu  26387  ig1pval3  26390  dgrle  26455  0dgrb  26458  dgreq0  26477  fta1lem  26523  fta1  26524  aannenlem1  26546  aannenlem2  26547  aalioulem2  26551  reeff1o  26665  eflogeq  26822  argregt0  26830  argrege0  26831  efopn  26878  asinsinb  27117  acoscosb  27118  atantanb  27144  musum  27410  dchrptlem1  27483  dchrptlem2  27484  lgsquadlem1  27599  nosupcbv  27921  nosupfv  27925  noinfcbv  27936  noinffv  27940  nocvxmin  28003  cutbday  28032  eqcuts  28033  cutsun12  28038  cutbdaylt  28046  cuteq0  28063  negleft  28306  negright  28307  oniso  28519  bdayn0sf1o  28618  dfnns2  28620  znegscl  28640  renegscl  28746  istrkgl  28782  mirreu  28996  israg  29032  lmireu  29154  lmieq  29155  gropd  29440  grstructd  29441  umgredg2  29509  umgrbi  29510  umgrnloopv  29515  umgredgprv  29516  edgumgr  29544  numedglnl  29553  umgredgnlp  29556  edgusgr  29572  usgruspgrb  29595  uhgr2edg  29620  usgredg2v  29639  ushgredgedgloop  29643  usgr1e  29657  usgrexmplef  29671  subumgredg2  29697  umgrreslem  29717  cusgrexilem2  29854  cusgrexg  29856  fusgrn0degnn0  29911  umgr2v2e  29937  vdiscusgr  29943  rusgr1vtxlem  29999  rgrusgrprc  30001  wlkon2n0  30076  upgrwlkdvdelem  30153  spthonepeq  30169  usgr2wlkneq  30173  iswwlksn  30258  wwlksnon  30271  wwlksn0  30283  wlkiswwlksupgr2  30297  wlknwwlksnbij  30308  wwlksnextbi  30314  wwlksnextfun  30318  wwlksnextinj  30319  wwlksnextbij  30322  2pthon3v  30363  umgr2wlk  30369  rusgrnumwwlkb0  30394  isclwwlkn  30449  clwwlkn1loopb  30465  hashecclwwlkn1  30499  s2elclwwlknon2  30526  loop1cycl  30575  umgr2cycl  30578  uhgr3cyclex  30608  frgrwopreglem4a  30736  frgrwopreglem3  30740  frgrwopreglem5lem  30746  frgrwopreglem5  30747  frgrregorufr0  30750  friendshipgt3  30824  nvz  31096  nmlno0i  31221  norm1exi  31677  pjoc1  31861  pjoc2  31866  pj11  32141  elnlfn  32355  nmlnop0  32425  adjbd1o  32512  strlem1  32677  stcltr1i  32701  2ndimaxp  33066  fnpreimac  33090  indf1ofs  33260  isarchi  33570  ply1dg1rt  33938  extvfval  33990  esplyfval0  34022  esplymhp  34026  esplyfv1  34027  vieta  34038  minplyval  34163  qtophaus  34294  locfinreflem  34298  rhmpreimacn  34343  isrrext  34458  eulerpartlemsv3  34820  eulerpartlemgvv  34835  ballotlemelo  34947  ballotlemfmpn  34954  ballotlemiex  34961  ballotlemi1  34962  ballotlemii  34963  ballotlemfrcn0  34989  ballotlemirc  34991  bnj229  35341  bnj517  35342  bnj590  35367  bnj1097  35438  bnj1118  35441  bnj1128  35447  bnj1145  35450  elscott2  35575  elscottrank  35576  kardeng  35631  vonf1oonfo  35660  subfacp1lem3  35715  cvmlift3lem5  35856  satffunlem1lem1  35935  satffunlem2lem1  35937  satffunlem2lem2  35939  mthmi  36110  rankeq1o  36704  weiunfr  37039  finxpreclem6  38103  poimirlem13  38345  poimirlem14  38346  poimirlem17  38349  poimirlem18  38350  poimirlem21  38353  poimirlem27  38359  poimirlem28  38360  ovoliunnfl  38374  voliunnfl  38376  volsupnfl  38377  lfl1  39906  lshpkrex  39954  cdleme50rnlem  41380  dochkr1  42314  dochkr1OLDN  42315  lcfrlem28  42406  mapd1o  42484  hdmap1vallem  42633  aks6d1c4  42953  hashnexinjle  42958  sticksstones2  42976  sticksstones3  42977  aks6d1c6lem3  43001  aks6d1c6isolem1  43003  aks6d1c6isolem2  43004  grpods  43023  unitscyglem1  43024  unitscyglem2  43025  unitscyglem3  43026  unitscyglem4  43027  unitscyglem5  43028  diophrw  43567  eldioph3  43574  diophin  43580  eq0rabdioph  43584  eldioph4b  43615  fphpdo  43621  fnwe2lem2  43855  fnwe2lem3  43856  islssfgi  43876  hbt  43934  dgraaval  43948  dgraalem  43949  dgraaub  43952  mpaaeu  43954  mpaaval  43955  mpaalem  43956  rngunsnply  43973  idomsubgmo  43997  proot1mul  43998  cantnfresb  44128  fvelrnbf  45815  wessf1ornlem  45980  sumnnodd  46423  fourierdlem2  46900  fourierdlem3  46901  fcoresf1  47883  uniimafveqt  48207  elsetpreimafvrab  48220  prpair  48327  prproropf1olem1  48329  pairreueq  48336  paireqne  48337  prprspr2  48344  reuprpr  48349  requad2  48465  cycldlenngric  48770  uhgrimisgrgriclem  48772  clnbgrgrimlem  48775  clnbgrgrim  48776  usgrgrtrirex  48792  stgrusgra  48801  uspgrlimlem1  48830  uspgrlimlem2  48831  grlimgrtri  48845  usgrexmpl1lem  48863  usgrexmpl2lem  48868  gpgusgralem  48898  gpgprismgr4cyclex  48949  uspgrsprfo  48990  ply1mulgsumlem2  49243  lindslinindsimp1  49313  snlindsntor  49327  nn0sumshdiglemA  49475  nn0sumshdiglemB  49476  nn0sumshdiglem1  49477  nn0sumshdig  49479  istermc  50328