Theorem fveqeq2 6792

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445

This theorem is referenced by:  fvelimad  6845  dff13f  7138  f1veqaeq  7139  f1elima  7145  fpropnf1  7149  nf1const  7185  oteqimp  7859  fimaproj  7985  suppfnss  8014  suppssfv  8027  tz7.48lem  8281  seqomlem1  8290  seqomlem2  8291  fofinf1o  9103  fipreima  9134  cantnfp1lem3  9447  brttrcl2  9481  ssttrcl  9482  ttrcltr  9483  tcrank  9651  updjudhcoinlf  9699  updjudhcoinrg  9700  pm54.43lem  9767  ackbij1lem18  10002  ackbij1  10003  axcc2  10202  iunfo  10304  grur1  10585  injresinjlem  13516  injresinj  13517  suppssfz  13723  seqid2  13778  hashrabsn01  14097  hashrabsn1  14098  hashimarni  14165  hashbclem  14173  hashbc  14174  hash2exprb  14194  elss2prb  14210  hash2sspr  14211  fi1uzind  14220  brfi1indALT  14223  wrdmap  14258  wrdl1s1  14328  wrdind  14444  wrd2ind  14445  reuccatpfxs1lem  14468  reuccatpfxs1  14469  cshf1  14532  cshw1  14544  wwlktovf  14680  wwlktovf1  14681  wwlktovfo  14682  wrd2f1tovbij  14684  wrdl3s3  14686  abs1m  15056  sumrblem  15432  fsumcvg  15433  summolem2a  15436  incexc2  15559  ntrivcvgfvn0  15620  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  smupvallem  16199  smu01lem  16201  algfx  16294  iserodd  16545  prmreclem2  16627  prmreclem3  16628  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  hashbcval  16712  ramub1lem1  16736  ramub1lem2  16737  imasleval  17261  eldmcoa  17789  coaval  17792  ghmf1  18872  orbsta  18928  symgextf1  19038  psgnunilem2  19112  psgnunilem3  19113  psgnunilem4  19114  odeq1  19176  odngen  19191  sylow1lem2  19213  sylow1lem4  19215  sylow1lem5  19216  pgpfi  19219  efgtlen  19341  efgsfo  19354  efgredlemd  19359  efgred  19363  gsummptnn0fzfv  19597  isabvd  20089  abveq0  20095  abvdom  20107  islbs  20347  isobs  20936  cply1mul  21474  mdetunilem1  21770  mdetunilem4  21773  mdetunilem8  21777  mdetunilem9  21778  pmatcoe1fsupp  21859  m2cpminvid2lem  21912  mp2pm2mplem4  21967  2ndci  22608  2ndcsb  22609  2ndcsep  22619  txkgen  22812  nmoeq0  23909  nmoleub3  24291  ivth  24627  ivthle  24629  ivthle2  24630  ovolunlem1  24670  ovolicc2  24695  volivth  24780  mbfinf  24838  itg2splitlem  24922  rollelem  25162  rolle  25163  tdeglem4  25233  tdeglem4OLD  25234  mdeglt  25239  deg1leb  25269  deg1lt  25271  fta1g  25341  ig1peu  25345  ig1pval3  25348  dgrle  25413  0dgrb  25416  dgreq0  25435  fta1lem  25476  fta1  25477  aannenlem1  25497  aannenlem2  25498  aalioulem2  25502  reeff1o  25615  eflogeq  25766  argregt0  25774  argrege0  25775  efopn  25822  asinsinb  26056  acoscosb  26057  atantanb  26083  musum  26349  dchrptlem1  26421  dchrptlem2  26422  lgsquadlem1  26537  istrkgl  26828  mirreu  27034  israg  27067  lmireu  27160  lmieq  27161  gropd  27410  grstructd  27411  umgredg2  27479  umgrbi  27480  umgrnloopv  27485  umgredgprv  27486  edgumgr  27514  numedglnl  27523  umgredgnlp  27526  edgusgr  27539  usgruspgrb  27560  uhgr2edg  27584  usgredg2v  27603  ushgredgedgloop  27607  usgr1e  27621  usgrexmplef  27635  subumgredg2  27661  umgrreslem  27681  cusgrexilem2  27818  cusgrexg  27820  fusgrn0degnn0  27875  umgr2v2e  27901  vdiscusgr  27907  rusgr1vtxlem  27963  rgrusgrprc  27965  wlkon2n0  28043  upgrwlkdvdelem  28113  spthonepeq  28129  usgr2wlkneq  28133  iswwlksn  28212  wwlksnon  28225  wwlksn0  28237  wlkiswwlksupgr2  28251  wlknwwlksnbij  28262  wwlksnextbi  28268  wwlksnextfun  28272  wwlksnextinj  28273  wwlksnextbij  28276  2pthon3v  28317  umgr2wlk  28323  rusgrnumwwlkb0  28345  isclwwlkn  28400  clwwlkn1loopb  28416  hashecclwwlkn1  28450  s2elclwwlknon2  28477  uhgr3cyclex  28555  frgrwopreglem4a  28683  frgrwopreglem3  28687  frgrwopreglem5lem  28693  frgrwopreglem5  28694  frgrregorufr0  28697  friendshipgt3  28771  nvz  29040  nmlno0i  29165  norm1exi  29621  pjoc1  29805  pjoc2  29810  pj11  30085  elnlfn  30299  nmlnop0  30369  adjbd1o  30456  strlem1  30621  stcltr1i  30645  2ndimaxp  30993  fnpreimac  31017  isarchi  31445  qtophaus  31795  locfinreflem  31799  rhmpreimacn  31844  isrrext  31959  indf1ofs  32003  eulerpartlemsv3  32337  eulerpartlemgvv  32352  ballotlemelo  32463  ballotlemfmpn  32470  ballotlemiex  32477  ballotlemi1  32478  ballotlemii  32479  ballotlemfrcn0  32505  ballotlemirc  32507  bnj229  32873  bnj517  32874  bnj590  32899  bnj1097  32970  bnj1118  32973  bnj1128  32979  bnj1145  32982  f1resfz0f1d  33081  loop1cycl  33108  umgr2cycl  33112  subfacp1lem3  33153  cvmlift3lem5  33294  satffunlem1lem1  33373  satffunlem2lem1  33375  satffunlem2lem2  33377  mthmi  33548  nosupcbv  33914  nosupfv  33918  noinfcbv  33929  noinffv  33933  nocvxmin  33982  scutbday  34007  eqscut  34008  scutun12  34013  scutbdaylt  34021  rankeq1o  34482  finxpreclem6  35576  poimirlem13  35799  poimirlem14  35800  poimirlem17  35803  poimirlem18  35804  poimirlem21  35807  poimirlem27  35813  poimirlem28  35814  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  lfl1  37091  lshpkrex  37139  cdleme50rnlem  38565  dochkr1  39499  dochkr1OLDN  39500  lcfrlem28  39591  mapd1o  39669  hdmap1vallem  39818  sticksstones2  40110  sticksstones3  40111  diophrw  40588  eldioph3  40595  diophin  40601  eq0rabdioph  40605  eldioph4b  40640  fphpdo  40646  fnwe2lem2  40883  fnwe2lem3  40884  islssfgi  40904  hbt  40962  dgraaval  40976  dgraalem  40977  dgraaub  40980  mpaaeu  40982  mpaaval  40983  mpaalem  40984  rngunsnply  41005  idomsubgmo  41030  proot1mul  41031  fvelrnbf  42568  wessf1ornlem  42729  sumnnodd  43178  fourierdlem2  43657  fourierdlem3  43658  fcoresf1  44574  uniimafveqt  44844  elsetpreimafvrab  44857  prpair  44964  prproropf1olem1  44966  pairreueq  44973  paireqne  44974  prprspr2  44981  reuprpr  44986  requad2  45086  uspgrsprfo  45321  ply1mulgsumlem2  45739  lindslinindsimp1  45809  snlindsntor  45823  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdiglem1  45978  nn0sumshdig  45980