Theorem fveqeq2 6849

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507

This theorem is referenced by:  fvelimad  6910  dff13f  7212  f1veqaeq  7213  f1elima  7220  fpropnf1  7224  nf1const  7261  oteqimp  7966  fimaproj  8091  suppfnss  8145  suppssfv  8158  tz7.48lem  8386  seqomlem1  8395  seqomlem2  8396  fofinf1o  9259  fipreima  9285  cantnfp1lem3  9609  brttrcl2  9643  ssttrcl  9644  ttrcltr  9645  tcrank  9813  updjudhcoinlf  9861  updjudhcoinrg  9862  pm54.43lem  9929  ackbij1lem18  10165  ackbij1  10166  axcc2  10366  iunfo  10468  grur1  10749  injresinjlem  13724  injresinj  13725  suppssfz  13935  seqid2  13989  hashrabsn01  14314  hashrabsn1  14315  hashimarni  14382  hashbclem  14393  hashbc  14394  hash2exprb  14412  elss2prb  14429  hash2sspr  14430  hash3tpde  14434  fi1uzind  14448  brfi1indALT  14451  wrdmap  14487  wrdl1s1  14555  wrdind  14663  wrd2ind  14664  reuccatpfxs1lem  14687  reuccatpfxs1  14688  cshf1  14751  cshw1  14763  wwlktovf  14898  wwlktovf1  14899  wwlktovfo  14900  wrd2f1tovbij  14902  wrdl3s3  14904  abs1m  15278  sumrblem  15653  fsumcvg  15654  summolem2a  15657  incexc2  15780  ntrivcvgfvn0  15841  prodrblem  15871  fprodcvg  15872  prodmolem2a  15876  smupvallem  16429  smu01lem  16431  algfx  16526  iserodd  16782  prmreclem2  16864  prmreclem3  16865  vdwlem2  16929  vdwlem6  16933  vdwlem8  16935  hashbcval  16949  ramub1lem1  16973  ramub1lem2  16974  imasleval  17480  eldmcoa  18007  coaval  18010  ghmf1  19160  ghmqusnsglem1  19194  ghmquskerlem1  19197  orbsta  19227  symgextf1  19335  psgnunilem2  19409  psgnunilem3  19410  psgnunilem4  19411  odeq1  19474  odngen  19491  sylow1lem2  19513  sylow1lem4  19515  sylow1lem5  19516  pgpfi  19519  efgtlen  19640  efgsfo  19653  efgredlemd  19658  efgred  19662  gsummptnn0fzfv  19901  isabvd  20732  abveq0  20738  abvdom  20750  islbs  21015  isobs  21662  cply1mul  22216  mdetunilem1  22532  mdetunilem4  22535  mdetunilem8  22539  mdetunilem9  22540  pmatcoe1fsupp  22621  m2cpminvid2lem  22674  mp2pm2mplem4  22729  2ndci  23368  2ndcsb  23369  2ndcsep  23379  txkgen  23572  nmoeq0  24657  nmoleub3  25052  ivth  25388  ivthle  25390  ivthle2  25391  ovolunlem1  25431  ovolicc2  25456  volivth  25541  mbfinf  25599  itg2splitlem  25682  rollelem  25926  rolle  25927  tdeglem4  25998  mdeglt  26003  deg1leb  26033  deg1lt  26035  fta1g  26108  ig1peu  26113  ig1pval3  26116  dgrle  26181  0dgrb  26184  dgreq0  26204  fta1lem  26248  fta1  26249  aannenlem1  26269  aannenlem2  26270  aalioulem2  26274  reeff1o  26390  eflogeq  26544  argregt0  26552  argrege0  26553  efopn  26600  asinsinb  26840  acoscosb  26841  atantanb  26867  musum  27134  dchrptlem1  27208  dchrptlem2  27209  lgsquadlem1  27324  nosupcbv  27647  nosupfv  27651  noinfcbv  27662  noinffv  27666  nocvxmin  27724  scutbday  27750  eqscut  27751  scutun12  27756  scutbdaylt  27764  cuteq0  27781  onsiso  28209  bdayn0sf1o  28299  dfnns2  28301  znegscl  28320  renegscl  28402  istrkgl  28438  mirreu  28644  israg  28677  lmireu  28770  lmieq  28771  gropd  29011  grstructd  29012  umgredg2  29080  umgrbi  29081  umgrnloopv  29086  umgredgprv  29087  edgumgr  29115  numedglnl  29124  umgredgnlp  29127  edgusgr  29140  usgruspgrb  29163  uhgr2edg  29188  usgredg2v  29207  ushgredgedgloop  29211  usgr1e  29225  usgrexmplef  29239  subumgredg2  29265  umgrreslem  29285  cusgrexilem2  29422  cusgrexg  29424  fusgrn0degnn0  29480  umgr2v2e  29506  vdiscusgr  29512  rusgr1vtxlem  29568  rgrusgrprc  29570  wlkon2n0  29645  upgrwlkdvdelem  29716  spthonepeq  29732  usgr2wlkneq  29736  iswwlksn  29818  wwlksnon  29831  wwlksn0  29843  wlkiswwlksupgr2  29857  wlknwwlksnbij  29868  wwlksnextbi  29874  wwlksnextfun  29878  wwlksnextinj  29879  wwlksnextbij  29882  2pthon3v  29923  umgr2wlk  29929  rusgrnumwwlkb0  29951  isclwwlkn  30006  clwwlkn1loopb  30022  hashecclwwlkn1  30056  s2elclwwlknon2  30083  uhgr3cyclex  30161  frgrwopreglem4a  30289  frgrwopreglem3  30293  frgrwopreglem5lem  30299  frgrwopreglem5  30300  frgrregorufr0  30303  friendshipgt3  30377  nvz  30648  nmlno0i  30773  norm1exi  31229  pjoc1  31413  pjoc2  31418  pj11  31693  elnlfn  31907  nmlnop0  31977  adjbd1o  32064  strlem1  32229  stcltr1i  32253  2ndimaxp  32620  fnpreimac  32645  indf1ofs  32839  isarchi  33151  ply1dg1rt  33541  minplyval  33688  qtophaus  33819  locfinreflem  33823  rhmpreimacn  33868  isrrext  33983  eulerpartlemsv3  34345  eulerpartlemgvv  34360  ballotlemelo  34472  ballotlemfmpn  34479  ballotlemiex  34486  ballotlemi1  34487  ballotlemii  34488  ballotlemfrcn0  34514  ballotlemirc  34516  bnj229  34867  bnj517  34868  bnj590  34893  bnj1097  34964  bnj1118  34967  bnj1128  34973  bnj1145  34976  f1resfz0f1d  35094  loop1cycl  35117  umgr2cycl  35121  subfacp1lem3  35162  cvmlift3lem5  35303  satffunlem1lem1  35382  satffunlem2lem1  35384  satffunlem2lem2  35386  mthmi  35557  rankeq1o  36152  weiunfr  36448  finxpreclem6  37377  poimirlem13  37620  poimirlem14  37621  poimirlem17  37624  poimirlem18  37625  poimirlem21  37628  poimirlem27  37634  poimirlem28  37635  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  lfl1  39056  lshpkrex  39104  cdleme50rnlem  40531  dochkr1  41465  dochkr1OLDN  41466  lcfrlem28  41557  mapd1o  41635  hdmap1vallem  41784  aks6d1c4  42105  hashnexinjle  42110  sticksstones2  42128  sticksstones3  42129  aks6d1c6lem3  42153  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  unitscyglem5  42180  diophrw  42740  eldioph3  42747  diophin  42753  eq0rabdioph  42757  eldioph4b  42792  fphpdo  42798  fnwe2lem2  43033  fnwe2lem3  43034  islssfgi  43054  hbt  43112  dgraaval  43126  dgraalem  43127  dgraaub  43130  mpaaeu  43132  mpaaval  43133  mpaalem  43134  rngunsnply  43151  idomsubgmo  43175  proot1mul  43176  cantnfresb  43306  fvelrnbf  45005  wessf1ornlem  45172  sumnnodd  45621  fourierdlem2  46100  fourierdlem3  46101  fcoresf1  47063  uniimafveqt  47375  elsetpreimafvrab  47388  prpair  47495  prproropf1olem1  47497  pairreueq  47504  paireqne  47505  prprspr2  47512  reuprpr  47517  requad2  47617  cycldlenngric  47921  uhgrimisgrgriclem  47923  clnbgrgrimlem  47926  clnbgrgrim  47927  usgrgrtrirex  47942  stgrusgra  47951  uspgrlimlem1  47980  uspgrlimlem2  47981  grlimgrtri  47988  usgrexmpl1lem  48005  usgrexmpl2lem  48010  gpgusgralem  48040  gpgprismgr4cyclex  48090  uspgrsprfo  48129  ply1mulgsumlem2  48369  lindslinindsimp1  48439  snlindsntor  48453  nn0sumshdiglemA  48601  nn0sumshdiglemB  48602  nn0sumshdiglem1  48603  nn0sumshdig  48605  istermc  49456