Theorem fveqeq2 6845

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ‘cfv 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6450  df-fv 6502

This theorem is referenced by:  fvelimad  6903  dff13f  7205  f1veqaeq  7206  f1elima  7213  fpropnf1  7217  nf1const  7254  oteqimp  7956  fimaproj  8080  suppfnss  8134  suppssfv  8147  tz7.48lem  8375  seqomlem1  8384  seqomlem2  8385  fofinf1o  9237  fipreima  9263  cantnfp1lem3  9596  brttrcl2  9630  ssttrcl  9631  ttrcltr  9632  tcrank  9803  updjudhcoinlf  9851  updjudhcoinrg  9852  pm54.43lem  9919  ackbij1lem18  10153  ackbij1  10154  axcc2  10354  iunfo  10456  grur1  10738  injresinjlem  13740  injresinj  13741  suppssfz  13951  seqid2  14005  hashrabsn01  14330  hashrabsn1  14331  hashimarni  14398  hashbclem  14409  hashbc  14410  hash2exprb  14428  elss2prb  14445  hash2sspr  14446  hash3tpde  14450  fi1uzind  14464  brfi1indALT  14467  wrdmap  14503  wrdl1s1  14572  wrdind  14679  wrd2ind  14680  reuccatpfxs1lem  14703  reuccatpfxs1  14704  cshf1  14767  cshw1  14779  wwlktovf  14913  wwlktovf1  14914  wwlktovfo  14915  wrd2f1tovbij  14917  wrdl3s3  14919  abs1m  15293  sumrblem  15668  fsumcvg  15669  summolem2a  15672  incexc2  15798  ntrivcvgfvn0  15859  prodrblem  15889  fprodcvg  15890  prodmolem2a  15894  smupvallem  16447  smu01lem  16449  algfx  16544  iserodd  16801  prmreclem2  16883  prmreclem3  16884  vdwlem2  16948  vdwlem6  16952  vdwlem8  16954  hashbcval  16968  ramub1lem1  16992  ramub1lem2  16993  imasleval  17500  eldmcoa  18027  coaval  18030  ghmf1  19216  ghmqusnsglem1  19250  ghmquskerlem1  19253  orbsta  19283  symgextf1  19391  psgnunilem2  19465  psgnunilem3  19466  psgnunilem4  19467  odeq1  19530  odngen  19547  sylow1lem2  19569  sylow1lem4  19571  sylow1lem5  19572  pgpfi  19575  efgtlen  19696  efgsfo  19709  efgredlemd  19714  efgred  19718  gsummptnn0fzfv  19957  isabvd  20784  abveq0  20790  abvdom  20802  islbs  21067  isobs  21714  cply1mul  22275  mdetunilem1  22591  mdetunilem4  22594  mdetunilem8  22598  mdetunilem9  22599  pmatcoe1fsupp  22680  m2cpminvid2lem  22733  mp2pm2mplem4  22788  2ndci  23427  2ndcsb  23428  2ndcsep  23438  txkgen  23631  nmoeq0  24715  nmoleub3  25100  ivth  25435  ivthle  25437  ivthle2  25438  ovolunlem1  25478  ovolicc2  25503  volivth  25588  mbfinf  25646  itg2splitlem  25729  rollelem  25970  rolle  25971  tdeglem4  26039  mdeglt  26044  deg1leb  26074  deg1lt  26076  fta1g  26149  ig1peu  26154  ig1pval3  26157  dgrle  26222  0dgrb  26225  dgreq0  26244  fta1lem  26288  fta1  26289  aannenlem1  26309  aannenlem2  26310  aalioulem2  26314  reeff1o  26429  eflogeq  26583  argregt0  26591  argrege0  26592  efopn  26639  asinsinb  26878  acoscosb  26879  atantanb  26905  musum  27172  dchrptlem1  27245  dchrptlem2  27246  lgsquadlem1  27361  nosupcbv  27684  nosupfv  27688  noinfcbv  27699  noinffv  27703  nocvxmin  27765  cutbday  27794  eqcuts  27795  cutsun12  27800  cutbdaylt  27808  cuteq0  27825  negleft  28068  negright  28069  oniso  28281  bdayn0sf1o  28380  dfnns2  28382  znegscl  28402  renegscl  28508  istrkgl  28544  mirreu  28750  israg  28783  lmireu  28876  lmieq  28877  gropd  29118  grstructd  29119  umgredg2  29187  umgrbi  29188  umgrnloopv  29193  umgredgprv  29194  edgumgr  29222  numedglnl  29231  umgredgnlp  29234  edgusgr  29247  usgruspgrb  29270  uhgr2edg  29295  usgredg2v  29314  ushgredgedgloop  29318  usgr1e  29332  usgrexmplef  29346  subumgredg2  29372  umgrreslem  29392  cusgrexilem2  29529  cusgrexg  29531  fusgrn0degnn0  29587  umgr2v2e  29613  vdiscusgr  29619  rusgr1vtxlem  29675  rgrusgrprc  29677  wlkon2n0  29752  upgrwlkdvdelem  29823  spthonepeq  29839  usgr2wlkneq  29843  iswwlksn  29925  wwlksnon  29938  wwlksn0  29950  wlkiswwlksupgr2  29964  wlknwwlksnbij  29975  wwlksnextbi  29981  wwlksnextfun  29985  wwlksnextinj  29986  wwlksnextbij  29989  2pthon3v  30030  umgr2wlk  30036  rusgrnumwwlkb0  30061  isclwwlkn  30116  clwwlkn1loopb  30132  hashecclwwlkn1  30166  s2elclwwlknon2  30193  uhgr3cyclex  30271  frgrwopreglem4a  30399  frgrwopreglem3  30403  frgrwopreglem5lem  30409  frgrwopreglem5  30410  frgrregorufr0  30413  friendshipgt3  30487  nvz  30759  nmlno0i  30884  norm1exi  31340  pjoc1  31524  pjoc2  31529  pj11  31804  elnlfn  32018  nmlnop0  32088  adjbd1o  32175  strlem1  32340  stcltr1i  32364  2ndimaxp  32738  fnpreimac  32762  indf1ofs  32945  isarchi  33262  ply1dg1rt  33659  extvfval  33695  esplyfval0  33727  esplymhp  33731  esplyfv1  33732  vieta  33743  minplyval  33869  qtophaus  34000  locfinreflem  34004  rhmpreimacn  34049  isrrext  34164  eulerpartlemsv3  34525  eulerpartlemgvv  34540  ballotlemelo  34652  ballotlemfmpn  34659  ballotlemiex  34666  ballotlemi1  34667  ballotlemii  34668  ballotlemfrcn0  34694  ballotlemirc  34696  bnj229  35046  bnj517  35047  bnj590  35072  bnj1097  35143  bnj1118  35146  bnj1128  35152  bnj1145  35155  f1resfz0f1d  35316  loop1cycl  35339  umgr2cycl  35343  subfacp1lem3  35384  cvmlift3lem5  35525  satffunlem1lem1  35604  satffunlem2lem1  35606  satffunlem2lem2  35608  mthmi  35779  rankeq1o  36373  weiunfr  36669  finxpreclem6  37730  poimirlem13  37972  poimirlem14  37973  poimirlem17  37976  poimirlem18  37977  poimirlem21  37980  poimirlem27  37986  poimirlem28  37987  ovoliunnfl  38001  voliunnfl  38003  volsupnfl  38004  lfl1  39534  lshpkrex  39582  cdleme50rnlem  41008  dochkr1  41942  dochkr1OLDN  41943  lcfrlem28  42034  mapd1o  42112  hdmap1vallem  42261  aks6d1c4  42581  hashnexinjle  42586  sticksstones2  42604  sticksstones3  42605  aks6d1c6lem3  42629  aks6d1c6isolem1  42631  aks6d1c6isolem2  42632  grpods  42651  unitscyglem1  42652  unitscyglem2  42653  unitscyglem3  42654  unitscyglem4  42655  unitscyglem5  42656  diophrw  43209  eldioph3  43216  diophin  43222  eq0rabdioph  43226  eldioph4b  43261  fphpdo  43267  fnwe2lem2  43501  fnwe2lem3  43502  islssfgi  43522  hbt  43580  dgraaval  43594  dgraalem  43595  dgraaub  43598  mpaaeu  43600  mpaaval  43601  mpaalem  43602  rngunsnply  43619  idomsubgmo  43643  proot1mul  43644  cantnfresb  43774  fvelrnbf  45471  wessf1ornlem  45637  sumnnodd  46082  fourierdlem2  46559  fourierdlem3  46560  fcoresf1  47533  uniimafveqt  47857  elsetpreimafvrab  47870  prpair  47977  prproropf1olem1  47979  pairreueq  47986  paireqne  47987  prprspr2  47994  reuprpr  47999  requad2  48115  cycldlenngric  48420  uhgrimisgrgriclem  48422  clnbgrgrimlem  48425  clnbgrgrim  48426  usgrgrtrirex  48442  stgrusgra  48451  uspgrlimlem1  48480  uspgrlimlem2  48481  grlimgrtri  48495  usgrexmpl1lem  48513  usgrexmpl2lem  48518  gpgusgralem  48548  gpgprismgr4cyclex  48599  uspgrsprfo  48640  ply1mulgsumlem2  48879  lindslinindsimp1  48949  snlindsntor  48963  nn0sumshdiglemA  49111  nn0sumshdiglemB  49112  nn0sumshdiglem1  49113  nn0sumshdig  49115  istermc  49965