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 6538

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 6494  df-fv 6546

This theorem is used by:  fvelimad  6952  dff13f  7259  f1veqaeq  7260  f1elima  7267  fpropnf1  7271  nf1const  7312  oteqimp  8020  fnwe2lem3  8147  fnwe2lem4  8148  fimaproj  8152  suppfnss  8206  suppssfv  8219  tz7.48lemOLD  8451  seqomlem1  8460  seqomlem2  8461  fofinf1o  9321  fipreima  9347  cantnfp1lem3  9681  brttrcl2  9715  ssttrcl  9716  ttrcltr  9717  tcrank  9901  updjudhcoinlf  10013  updjudhcoinrg  10014  pm54.43lem  10081  ackbij1lem18  10314  ackbij1  10315  axcc2  10515  iunfo  10623  grur1  10905  injresinjlem  13925  injresinj  13926  f1resfz0f1d  13927  suppssfz  14137  seqid2  14191  hashrabsn01  14517  hashrabsn1  14518  hashimarni  14586  hashbclem  14597  hashbc  14598  hash2exprb  14616  elss2prb  14633  hash2sspr  14634  hash3tpde  14638  fi1uzind  14652  brfi1indALT  14655  wrdmap  14691  wrdl1s1  14762  wrdind  14871  wrd2ind  14872  reuccatpfxs1lem  14895  reuccatpfxs1  14896  cshf1  14961  cshw1  14973  wwlktovf  15109  wwlktovf1  15110  wwlktovfo  15111  wrd2f1tovbij  15113  wrdl3s3  15115  abs1m  15503  sumrblem  15877  fsumcvg  15878  summolem2a  15881  incexc2  16007  ntrivcvgfvn0  16068  prodrblem  16096  fprodcvg  16097  prodmolem2a  16101  smupvallem  16653  smu01lem  16655  algfx  16755  iserodd  17013  prmreclem2  17095  prmreclem3  17096  vdwlem2  17160  vdwlem6  17164  vdwlem8  17166  hashbcval  17180  ramub1lem1  17204  ramub1lem2  17205  imasleval  17713  eldmcoa  18240  coaval  18243  ghmf1  19460  ghmqusnsglem1  19494  ghmquskerlem1  19497  orbsta  19527  symgextf1  19635  psgnunilem2  19709  psgnunilem3  19710  psgnunilem4  19711  odeq1  19774  odngen  19791  sylow1lem2  19813  sylow1lem4  19815  sylow1lem5  19816  pgpfi  19819  efgtlen  19940  efgsfo  19953  efgredlemd  19958  efgred  19962  gsummptnn0fzfv  20201  isabvd  21069  abveq0  21075  abvdom  21087  islbs  21351  isobs  22026  cply1mul  22614  mdetunilem1  22927  mdetunilem4  22930  mdetunilem8  22934  mdetunilem9  22935  pmatcoe1fsupp  23019  m2cpminvid2lem  23072  mp2pm2mplem4  23127  2ndci  23766  2ndcsb  23767  2ndcsep  23778  txkgen  23971  nmoeq0  25055  nmoleub3  25440  ivth  25775  ivthle  25777  ivthle2  25778  ovolunlem1  25818  ovolicc2  25843  volivth  25928  mbfinf  25986  itg2splitlem  26069  rollelem  26309  rolle  26310  tdeglem4  26378  mdeglt  26383  deg1leb  26413  deg1lt  26415  fta1g  26488  ig1peu  26493  ig1pval3  26496  dgrle  26562  0dgrb  26565  dgreq0  26584  fta1lem  26628  fta1  26629  rnplynfin  26630  plyconz  26631  aannenlem1  26655  aannenlem2  26656  aalioulem2  26660  reeff1o  26774  eflogeq  26930  argregt0  26938  argrege0  26939  efopn  26986  asinsinb  27225  acoscosb  27226  atantanb  27252  musum  27518  dchrptlem1  27591  dchrptlem2  27592  lgsquadlem1  27707  nosupcbv  28059  nosupfv  28063  noinfcbv  28074  noinffv  28078  nocvxmin  28141  cutbday  28170  eqcuts  28171  cutsun12  28176  cutbdaylt  28184  cuteq0  28201  negleft  28444  negright  28445  oniso  28657  bdayn0sf1o  28756  dfnns2  28758  znegscl  28778  renegscl  28884  istrkgl  28920  mirreu  29136  israg  29172  lmireu  29295  lmieq  29296  gropd  29609  grstructd  29610  umgredg2  29678  umgrbi  29679  umgrnloopv  29684  umgredgprv  29685  edgumgr  29713  numedglnl  29722  umgredgnlp  29725  edgusgr  29741  usgruspgrb  29764  uhgr2edg  29789  usgredg2v  29808  ushgredgedgloop  29812  usgr1e  29826  usgrexmplef  29840  subumgredg2  29866  umgrreslem  29886  cusgrexilem2  30023  cusgrexg  30025  fusgrn0degnn0  30080  umgr2v2e  30106  vdiscusgr  30112  rusgr1vtxlem  30168  rgrusgrprc  30170  wlkon2n0  30245  upgrwlkdvdelem  30322  spthonepeq  30338  usgr2wlkneq  30342  iswwlksn  30427  wwlksnon  30440  wwlksn0  30452  wlkiswwlksupgr2  30466  wlknwwlksnbij  30477  wwlksnextbi  30483  wwlksnextfun  30487  wwlksnextinj  30488  wwlksnextbij  30491  2pthon3v  30532  umgr2wlk  30538  rusgrnumwwlkb0  30563  isclwwlkn  30618  clwwlkn1loopb  30634  hashecclwwlkn1  30668  s2elclwwlknon2  30695  loop1cycl  30744  umgr2cycl  30747  uhgr3cyclex  30783  frgrwopreglem4a  30911  frgrwopreglem3  30915  frgrwopreglem5lem  30921  frgrwopreglem5  30922  frgrregorufr0  30925  friendshipgt3  30999  nvz  31271  nmlno0i  31396  norm1exi  31852  pjoc1  32036  pjoc2  32041  pj11  32316  elnlfn  32530  nmlnop0  32600  adjbd1o  32687  strlem1  32852  stcltr1i  32876  2ndimaxp  33240  fnpreimac  33264  indf1ofs  33433  isarchi  33743  ply1dg1rt  34112  extvfval  34164  esplyfval0  34196  esplymhp  34200  esplyfv1  34201  vieta  34212  minplyval  34337  qtophaus  34468  locfinreflem  34472  rhmpreimacn  34517  isrrext  34632  eulerpartlemsv3  34993  eulerpartlemgvv  35008  ballotlemelo  35120  ballotlemfmpn  35127  ballotlemiex  35134  ballotlemi1  35135  ballotlemii  35136  ballotlemfrcn0  35162  ballotlemirc  35164  bnj229  35514  bnj517  35515  bnj590  35540  bnj1097  35611  bnj1118  35614  bnj1128  35620  bnj1145  35623  werankwe  35739  elscott2  35744  elscottrank  35745  acwer1prc  35760  kardeng  35825  vonf1oonfo  35898  subfacp1lem3  35947  cvmlift3lem5  36088  satffunlem1lem1  36167  satffunlem2lem1  36169  satffunlem2lem2  36171  mthmi  36342  rankeq1o  36932  weiunfr  37255  finxpreclem6  38319  poimirlem13  38551  poimirlem14  38552  poimirlem17  38555  poimirlem18  38556  poimirlem21  38559  poimirlem27  38565  poimirlem28  38566  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  lfl1  40127  lshpkrex  40175  cdleme50rnlem  41601  dochkr1  42535  dochkr1OLDN  42536  lcfrlem28  42627  mapd1o  42705  hdmap1vallem  42854  aks6d1c4  43174  hashnexinjle  43179  sticksstones2  43197  sticksstones3  43198  aks6d1c6lem3  43222  aks6d1c6isolem1  43224  aks6d1c6isolem2  43225  grpods  43244  unitscyglem1  43245  unitscyglem2  43246  unitscyglem3  43247  unitscyglem4  43248  unitscyglem5  43249  prjspnnorm  43661  diophrw  43769  eldioph3  43776  diophin  43782  eq0rabdioph  43786  eldioph4b  43817  fphpdo  43823  islssfgi  44073  hbt  44131  dgraaval  44145  dgraalem  44146  dgraaub  44149  mpaaeu  44151  mpaaval  44152  mpaalem  44153  rngunsnply  44170  idomsubgmo  44194  proot1mul  44195  cantnfresb  44325  fvelrnbf  46034  wessf1ornlem  46199  sumnnodd  46641  fourierdlem2  47118  fourierdlem3  47119  fcoresf1  48138  uniimafveqt  48462  elsetpreimafvrab  48475  prpair  48582  prproropf1olem1  48584  pairreueq  48591  paireqne  48592  prprspr2  48599  reuprpr  48604  requad2  48720  cycldlenngric  49025  uhgrimisgrgriclem  49027  clnbgrgrimlem  49030  clnbgrgrim  49031  usgrgrtrirex  49047  stgrusgra  49056  uspgrlimlem1  49085  uspgrlimlem2  49086  grlimgrtri  49100  usgrexmpl1lem  49118  usgrexmpl2lem  49123  gpgusgralem  49153  gpgprismgr4cyclex  49204  uspgrsprfo  49245  ply1mulgsumlem2  49498  lindslinindsimp1  49568  snlindsntor  49582  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdiglem1  49732  nn0sumshdig  49734  istermc  50581