Theorem fveqeq2 6888

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 6887	1 ⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

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

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

This theorem is used by:  fvelimad  6946  dff13f  7253  f1veqaeq  7254  f1elima  7261  fpropnf1  7265  nf1const  7306  oteqimp  8006  fimaproj  8134  suppfnss  8188  suppssfv  8201  tz7.48lemOLD  8433  seqomlem1  8442  seqomlem2  8443  fofinf1o  9302  fipreima  9328  cantnfp1lem3  9662  brttrcl2  9696  ssttrcl  9697  ttrcltr  9698  tcrank  9869  updjudhcoinlf  9940  updjudhcoinrg  9941  pm54.43lem  10008  ackbij1lem18  10241  ackbij1  10242  axcc2  10442  iunfo  10550  grur1  10832  injresinjlem  13849  injresinj  13850  f1resfz0f1d  13851  suppssfz  14061  seqid2  14115  hashrabsn01  14440  hashrabsn1  14441  hashimarni  14509  hashbclem  14520  hashbc  14521  hash2exprb  14539  elss2prb  14556  hash2sspr  14557  hash3tpde  14561  fi1uzind  14575  brfi1indALT  14578  wrdmap  14614  wrdl1s1  14685  wrdind  14794  wrd2ind  14795  reuccatpfxs1lem  14818  reuccatpfxs1  14819  cshf1  14884  cshw1  14896  wwlktovf  15032  wwlktovf1  15033  wwlktovfo  15034  wrd2f1tovbij  15036  wrdl3s3  15038  abs1m  15426  sumrblem  15800  fsumcvg  15801  summolem2a  15804  incexc2  15930  ntrivcvgfvn0  15991  prodrblem  16019  fprodcvg  16020  prodmolem2a  16024  smupvallem  16576  smu01lem  16578  algfx  16673  iserodd  16930  prmreclem2  17012  prmreclem3  17013  vdwlem2  17077  vdwlem6  17081  vdwlem8  17083  hashbcval  17097  ramub1lem1  17121  ramub1lem2  17122  imasleval  17630  eldmcoa  18157  coaval  18160  ghmf1  19376  ghmqusnsglem1  19410  ghmquskerlem1  19413  orbsta  19443  symgextf1  19551  psgnunilem2  19625  psgnunilem3  19626  psgnunilem4  19627  odeq1  19690  odngen  19707  sylow1lem2  19729  sylow1lem4  19731  sylow1lem5  19732  pgpfi  19735  efgtlen  19856  efgsfo  19869  efgredlemd  19874  efgred  19878  gsummptnn0fzfv  20117  isabvd  20981  abveq0  20987  abvdom  20999  islbs  21263  isobs  21936  cply1mul  22524  mdetunilem1  22837  mdetunilem4  22840  mdetunilem8  22844  mdetunilem9  22845  pmatcoe1fsupp  22929  m2cpminvid2lem  22982  mp2pm2mplem4  23037  2ndci  23676  2ndcsb  23677  2ndcsep  23688  txkgen  23881  nmoeq0  24965  nmoleub3  25350  ivth  25685  ivthle  25687  ivthle2  25688  ovolunlem1  25728  ovolicc2  25753  volivth  25838  mbfinf  25896  itg2splitlem  25979  rollelem  26219  rolle  26220  tdeglem4  26288  mdeglt  26293  deg1leb  26323  deg1lt  26325  fta1g  26398  ig1peu  26403  ig1pval3  26406  dgrle  26472  0dgrb  26475  dgreq0  26494  fta1lem  26540  fta1  26541  rnplynfin  26542  plyconz  26543  aannenlem1  26567  aannenlem2  26568  aalioulem2  26572  reeff1o  26686  eflogeq  26842  argregt0  26850  argrege0  26851  efopn  26898  asinsinb  27137  acoscosb  27138  atantanb  27164  musum  27430  dchrptlem1  27503  dchrptlem2  27504  lgsquadlem1  27619  nosupcbv  27941  nosupfv  27945  noinfcbv  27956  noinffv  27960  nocvxmin  28023  cutbday  28052  eqcuts  28053  cutsun12  28058  cutbdaylt  28066  cuteq0  28083  negleft  28326  negright  28327  oniso  28539  bdayn0sf1o  28638  dfnns2  28640  znegscl  28660  renegscl  28766  istrkgl  28802  mirreu  29018  israg  29054  lmireu  29177  lmieq  29178  gropd  29491  grstructd  29492  umgredg2  29560  umgrbi  29561  umgrnloopv  29566  umgredgprv  29567  edgumgr  29595  numedglnl  29604  umgredgnlp  29607  edgusgr  29623  usgruspgrb  29646  uhgr2edg  29671  usgredg2v  29690  ushgredgedgloop  29694  usgr1e  29708  usgrexmplef  29722  subumgredg2  29748  umgrreslem  29768  cusgrexilem2  29905  cusgrexg  29907  fusgrn0degnn0  29962  umgr2v2e  29988  vdiscusgr  29994  rusgr1vtxlem  30050  rgrusgrprc  30052  wlkon2n0  30127  upgrwlkdvdelem  30204  spthonepeq  30220  usgr2wlkneq  30224  iswwlksn  30309  wwlksnon  30322  wwlksn0  30334  wlkiswwlksupgr2  30348  wlknwwlksnbij  30359  wwlksnextbi  30365  wwlksnextfun  30369  wwlksnextinj  30370  wwlksnextbij  30373  2pthon3v  30414  umgr2wlk  30420  rusgrnumwwlkb0  30445  isclwwlkn  30500  clwwlkn1loopb  30516  hashecclwwlkn1  30550  s2elclwwlknon2  30577  loop1cycl  30626  umgr2cycl  30629  uhgr3cyclex  30665  frgrwopreglem4a  30793  frgrwopreglem3  30797  frgrwopreglem5lem  30803  frgrwopreglem5  30804  frgrregorufr0  30807  friendshipgt3  30881  nvz  31153  nmlno0i  31278  norm1exi  31734  pjoc1  31918  pjoc2  31923  pj11  32198  elnlfn  32412  nmlnop0  32482  adjbd1o  32569  strlem1  32734  stcltr1i  32758  2ndimaxp  33122  fnpreimac  33146  indf1ofs  33315  isarchi  33625  ply1dg1rt  33993  extvfval  34045  esplyfval0  34077  esplymhp  34081  esplyfv1  34082  vieta  34093  minplyval  34218  qtophaus  34349  locfinreflem  34353  rhmpreimacn  34398  isrrext  34513  eulerpartlemsv3  34875  eulerpartlemgvv  34890  ballotlemelo  35002  ballotlemfmpn  35009  ballotlemiex  35016  ballotlemi1  35017  ballotlemii  35018  ballotlemfrcn0  35044  ballotlemirc  35046  bnj229  35396  bnj517  35397  bnj590  35422  bnj1097  35493  bnj1118  35496  bnj1128  35502  bnj1145  35505  elscott2  35630  elscottrank  35631  kardeng  35686  vonf1oonfo  35715  subfacp1lem3  35764  cvmlift3lem5  35905  satffunlem1lem1  35984  satffunlem2lem1  35986  satffunlem2lem2  35988  mthmi  36159  rankeq1o  36754  weiunfr  37089  finxpreclem6  38153  poimirlem13  38385  poimirlem14  38386  poimirlem17  38389  poimirlem18  38390  poimirlem21  38393  poimirlem27  38399  poimirlem28  38400  ovoliunnfl  38414  voliunnfl  38416  volsupnfl  38417  lfl1  39946  lshpkrex  39994  cdleme50rnlem  41420  dochkr1  42354  dochkr1OLDN  42355  lcfrlem28  42446  mapd1o  42524  hdmap1vallem  42673  aks6d1c4  42993  hashnexinjle  42998  sticksstones2  43016  sticksstones3  43017  aks6d1c6lem3  43041  aks6d1c6isolem1  43043  aks6d1c6isolem2  43044  grpods  43063  unitscyglem1  43064  unitscyglem2  43065  unitscyglem3  43066  unitscyglem4  43067  unitscyglem5  43068  diophrw  43607  eldioph3  43614  diophin  43620  eq0rabdioph  43624  eldioph4b  43655  fphpdo  43661  fnwe2lem2  43895  fnwe2lem3  43896  islssfgi  43916  hbt  43974  dgraaval  43988  dgraalem  43989  dgraaub  43992  mpaaeu  43994  mpaaval  43995  mpaalem  43996  rngunsnply  44013  idomsubgmo  44037  proot1mul  44038  cantnfresb  44168  fvelrnbf  45855  wessf1ornlem  46020  sumnnodd  46463  fourierdlem2  46940  fourierdlem3  46941  fcoresf1  47960  uniimafveqt  48284  elsetpreimafvrab  48297  prpair  48404  prproropf1olem1  48406  pairreueq  48413  paireqne  48414  prprspr2  48421  reuprpr  48426  requad2  48542  cycldlenngric  48847  uhgrimisgrgriclem  48849  clnbgrgrimlem  48852  clnbgrgrim  48853  usgrgrtrirex  48869  stgrusgra  48878  uspgrlimlem1  48907  uspgrlimlem2  48908  grlimgrtri  48922  usgrexmpl1lem  48940  usgrexmpl2lem  48945  gpgusgralem  48975  gpgprismgr4cyclex  49026  uspgrsprfo  49067  ply1mulgsumlem2  49320  lindslinindsimp1  49390  snlindsntor  49404  nn0sumshdiglemA  49552  nn0sumshdiglemB  49553  nn0sumshdiglem1  49554  nn0sumshdig  49556  istermc  50403