Theorem fveqeq2 6891

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545

This theorem is referenced by:  fvelimad  6949  dff13f  7254  f1veqaeq  7255  f1elima  7262  fpropnf1  7266  nf1const  7303  oteqimp  8005  fimaproj  8131  suppfnss  8185  suppssfv  8198  tz7.48lem  8428  seqomlem1  8437  seqomlem2  8438  fofinf1o  9289  fipreima  9315  cantnfp1lem3  9649  brttrcl2  9683  ssttrcl  9684  ttrcltr  9685  tcrank  9856  updjudhcoinlf  9918  updjudhcoinrg  9919  pm54.43lem  9986  ackbij1lem18  10219  ackbij1  10220  axcc2  10421  iunfo  10523  grur1  10805  injresinjlem  13819  injresinj  13820  suppssfz  14030  seqid2  14084  hashrabsn01  14409  hashrabsn1  14410  hashimarni  14478  hashbclem  14489  hashbc  14490  hash2exprb  14508  elss2prb  14525  hash2sspr  14526  hash3tpde  14530  fi1uzind  14544  brfi1indALT  14547  wrdmap  14583  wrdl1s1  14652  wrdind  14759  wrd2ind  14760  reuccatpfxs1lem  14783  reuccatpfxs1  14784  cshf1  14847  cshw1  14859  wwlktovf  14993  wwlktovf1  14994  wwlktovfo  14995  wrd2f1tovbij  14997  wrdl3s3  14999  abs1m  15387  sumrblem  15762  fsumcvg  15763  summolem2a  15766  incexc2  15892  ntrivcvgfvn0  15953  prodrblem  15983  fprodcvg  15984  prodmolem2a  15988  smupvallem  16541  smu01lem  16543  algfx  16638  iserodd  16895  prmreclem2  16977  prmreclem3  16978  vdwlem2  17042  vdwlem6  17046  vdwlem8  17048  hashbcval  17062  ramub1lem1  17086  ramub1lem2  17087  imasleval  17595  eldmcoa  18122  coaval  18125  ghmf1  19316  ghmqusnsglem1  19350  ghmquskerlem1  19353  orbsta  19383  symgextf1  19491  psgnunilem2  19565  psgnunilem3  19566  psgnunilem4  19567  odeq1  19630  odngen  19647  sylow1lem2  19669  sylow1lem4  19671  sylow1lem5  19672  pgpfi  19675  efgtlen  19796  efgsfo  19809  efgredlemd  19814  efgred  19818  gsummptnn0fzfv  20057  isabvd  20893  abveq0  20899  abvdom  20911  islbs  21175  isobs  21839  cply1mul  22425  mdetunilem1  22738  mdetunilem4  22741  mdetunilem8  22745  mdetunilem9  22746  pmatcoe1fsupp  22827  m2cpminvid2lem  22880  mp2pm2mplem4  22935  2ndci  23574  2ndcsb  23575  2ndcsep  23585  txkgen  23778  nmoeq0  24862  nmoleub3  25247  ivth  25582  ivthle  25584  ivthle2  25585  ovolunlem1  25625  ovolicc2  25650  volivth  25735  mbfinf  25793  itg2splitlem  25876  rollelem  26117  rolle  26118  tdeglem4  26186  mdeglt  26191  deg1leb  26221  deg1lt  26223  fta1g  26296  ig1peu  26301  ig1pval3  26304  dgrle  26369  0dgrb  26372  dgreq0  26391  fta1lem  26437  fta1  26438  aannenlem1  26458  aannenlem2  26459  aalioulem2  26463  reeff1o  26576  eflogeq  26733  argregt0  26741  argrege0  26742  efopn  26789  asinsinb  27028  acoscosb  27029  atantanb  27055  musum  27321  dchrptlem1  27394  dchrptlem2  27395  lgsquadlem1  27510  nosupcbv  27832  nosupfv  27836  noinfcbv  27847  noinffv  27851  nocvxmin  27914  cutbday  27943  eqcuts  27944  cutsun12  27949  cutbdaylt  27957  cuteq0  27974  negleft  28217  negright  28218  oniso  28430  bdayn0sf1o  28529  dfnns2  28531  znegscl  28551  renegscl  28657  istrkgl  28693  mirreu  28903  israg  28936  lmireu  29057  lmieq  29058  gropd  29322  grstructd  29323  umgredg2  29391  umgrbi  29392  umgrnloopv  29397  umgredgprv  29398  edgumgr  29426  numedglnl  29435  umgredgnlp  29438  edgusgr  29451  usgruspgrb  29474  uhgr2edg  29499  usgredg2v  29518  ushgredgedgloop  29522  usgr1e  29536  usgrexmplef  29550  subumgredg2  29576  umgrreslem  29596  cusgrexilem2  29733  cusgrexg  29735  fusgrn0degnn0  29790  umgr2v2e  29816  vdiscusgr  29822  rusgr1vtxlem  29878  rgrusgrprc  29880  wlkon2n0  29955  upgrwlkdvdelem  30026  spthonepeq  30042  usgr2wlkneq  30046  iswwlksn  30128  wwlksnon  30141  wwlksn0  30153  wlkiswwlksupgr2  30167  wlknwwlksnbij  30178  wwlksnextbi  30184  wwlksnextfun  30188  wwlksnextinj  30189  wwlksnextbij  30192  2pthon3v  30233  umgr2wlk  30239  rusgrnumwwlkb0  30264  isclwwlkn  30319  clwwlkn1loopb  30335  hashecclwwlkn1  30369  s2elclwwlknon2  30396  uhgr3cyclex  30474  frgrwopreglem4a  30602  frgrwopreglem3  30606  frgrwopreglem5lem  30612  frgrwopreglem5  30613  frgrregorufr0  30616  friendshipgt3  30690  nvz  30962  nmlno0i  31087  norm1exi  31543  pjoc1  31727  pjoc2  31732  pj11  32007  elnlfn  32221  nmlnop0  32291  adjbd1o  32378  strlem1  32543  stcltr1i  32567  2ndimaxp  32932  fnpreimac  32956  indf1ofs  33127  isarchi  33443  ply1dg1rt  33815  extvfval  33867  esplyfval0  33899  esplymhp  33903  esplyfv1  33904  vieta  33915  minplyval  34040  qtophaus  34171  locfinreflem  34175  rhmpreimacn  34220  isrrext  34335  eulerpartlemsv3  34696  eulerpartlemgvv  34711  ballotlemelo  34823  ballotlemfmpn  34830  ballotlemiex  34837  ballotlemi1  34838  ballotlemii  34839  ballotlemfrcn0  34865  ballotlemirc  34867  bnj229  35217  bnj517  35218  bnj590  35243  bnj1097  35314  bnj1118  35317  bnj1128  35323  bnj1145  35326  kardeng  35503  vonf1oonfo  35532  f1resfz0f1d  35538  loop1cycl  35562  umgr2cycl  35566  subfacp1lem3  35607  cvmlift3lem5  35748  satffunlem1lem1  35827  satffunlem2lem1  35829  satffunlem2lem2  35831  mthmi  36002  rankeq1o  36596  weiunfr  36901  finxpreclem6  37964  poimirlem13  38206  poimirlem14  38207  poimirlem17  38210  poimirlem18  38211  poimirlem21  38214  poimirlem27  38220  poimirlem28  38221  ovoliunnfl  38235  voliunnfl  38237  volsupnfl  38238  lfl1  39768  lshpkrex  39816  cdleme50rnlem  41242  dochkr1  42176  dochkr1OLDN  42177  lcfrlem28  42268  mapd1o  42346  hdmap1vallem  42495  aks6d1c4  42815  hashnexinjle  42820  sticksstones2  42838  sticksstones3  42839  aks6d1c6lem3  42863  aks6d1c6isolem1  42865  aks6d1c6isolem2  42866  grpods  42885  unitscyglem1  42886  unitscyglem2  42887  unitscyglem3  42888  unitscyglem4  42889  unitscyglem5  42890  diophrw  43416  eldioph3  43423  diophin  43429  eq0rabdioph  43433  eldioph4b  43464  fphpdo  43470  fnwe2lem2  43704  fnwe2lem3  43705  islssfgi  43725  hbt  43783  dgraaval  43797  dgraalem  43798  dgraaub  43801  mpaaeu  43803  mpaaval  43804  mpaalem  43805  rngunsnply  43822  idomsubgmo  43846  proot1mul  43847  cantnfresb  43977  fvelrnbf  45664  wessf1ornlem  45829  sumnnodd  46272  fourierdlem2  46749  fourierdlem3  46750  fcoresf1  47729  uniimafveqt  48053  elsetpreimafvrab  48066  prpair  48173  prproropf1olem1  48175  pairreueq  48182  paireqne  48183  prprspr2  48190  reuprpr  48195  requad2  48311  cycldlenngric  48616  uhgrimisgrgriclem  48618  clnbgrgrimlem  48621  clnbgrgrim  48622  usgrgrtrirex  48638  stgrusgra  48647  uspgrlimlem1  48676  uspgrlimlem2  48677  grlimgrtri  48691  usgrexmpl1lem  48709  usgrexmpl2lem  48714  gpgusgralem  48744  gpgprismgr4cyclex  48795  uspgrsprfo  48836  ply1mulgsumlem2  49086  lindslinindsimp1  49156  snlindsntor  49170  nn0sumshdiglemA  49318  nn0sumshdiglemB  49319  nn0sumshdiglem1  49320  nn0sumshdig  49322  istermc  50171