Theorem fveqeq2 6895

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549

This theorem is referenced by:  fvelimad  6956  dff13f  7258  f1veqaeq  7259  f1elima  7265  fpropnf1  7269  nf1const  7306  oteqimp  8015  fimaproj  8142  suppfnss  8196  suppssfv  8209  tz7.48lem  8463  seqomlem1  8472  seqomlem2  8473  fofinf1o  9354  fipreima  9380  cantnfp1lem3  9702  brttrcl2  9736  ssttrcl  9737  ttrcltr  9738  tcrank  9906  updjudhcoinlf  9954  updjudhcoinrg  9955  pm54.43lem  10022  ackbij1lem18  10258  ackbij1  10259  axcc2  10459  iunfo  10561  grur1  10842  injresinjlem  13808  injresinj  13809  suppssfz  14017  seqid2  14071  hashrabsn01  14395  hashrabsn1  14396  hashimarni  14463  hashbclem  14474  hashbc  14475  hash2exprb  14493  elss2prb  14510  hash2sspr  14511  hash3tpde  14515  fi1uzind  14529  brfi1indALT  14532  wrdmap  14567  wrdl1s1  14635  wrdind  14743  wrd2ind  14744  reuccatpfxs1lem  14767  reuccatpfxs1  14768  cshf1  14831  cshw1  14843  wwlktovf  14978  wwlktovf1  14979  wwlktovfo  14980  wrd2f1tovbij  14982  wrdl3s3  14984  abs1m  15357  sumrblem  15730  fsumcvg  15731  summolem2a  15734  incexc2  15857  ntrivcvgfvn0  15918  prodrblem  15948  fprodcvg  15949  prodmolem2a  15953  smupvallem  16503  smu01lem  16505  algfx  16600  iserodd  16856  prmreclem2  16938  prmreclem3  16939  vdwlem2  17003  vdwlem6  17007  vdwlem8  17009  hashbcval  17023  ramub1lem1  17047  ramub1lem2  17048  imasleval  17558  eldmcoa  18082  coaval  18085  ghmf1  19234  ghmqusnsglem1  19268  ghmquskerlem1  19271  orbsta  19301  symgextf1  19408  psgnunilem2  19482  psgnunilem3  19483  psgnunilem4  19484  odeq1  19547  odngen  19564  sylow1lem2  19586  sylow1lem4  19588  sylow1lem5  19589  pgpfi  19592  efgtlen  19713  efgsfo  19726  efgredlemd  19731  efgred  19735  gsummptnn0fzfv  19974  isabvd  20782  abveq0  20788  abvdom  20800  islbs  21044  isobs  21695  cply1mul  22249  mdetunilem1  22567  mdetunilem4  22570  mdetunilem8  22574  mdetunilem9  22575  pmatcoe1fsupp  22656  m2cpminvid2lem  22709  mp2pm2mplem4  22764  2ndci  23403  2ndcsb  23404  2ndcsep  23414  txkgen  23607  nmoeq0  24694  nmoleub3  25089  ivth  25426  ivthle  25428  ivthle2  25429  ovolunlem1  25469  ovolicc2  25494  volivth  25579  mbfinf  25637  itg2splitlem  25720  rollelem  25964  rolle  25965  tdeglem4  26036  mdeglt  26041  deg1leb  26071  deg1lt  26073  fta1g  26146  ig1peu  26151  ig1pval3  26154  dgrle  26219  0dgrb  26222  dgreq0  26242  fta1lem  26286  fta1  26287  aannenlem1  26307  aannenlem2  26308  aalioulem2  26312  reeff1o  26428  eflogeq  26581  argregt0  26589  argrege0  26590  efopn  26637  asinsinb  26877  acoscosb  26878  atantanb  26904  musum  27171  dchrptlem1  27245  dchrptlem2  27246  lgsquadlem1  27361  nosupcbv  27684  nosupfv  27688  noinfcbv  27699  noinffv  27703  nocvxmin  27760  scutbday  27786  eqscut  27787  scutun12  27792  scutbdaylt  27800  cuteq0  27814  dfnns2  28299  znegscl  28315  renegscl  28367  istrkgl  28403  mirreu  28609  israg  28642  lmireu  28735  lmieq  28736  gropd  28977  grstructd  28978  umgredg2  29046  umgrbi  29047  umgrnloopv  29052  umgredgprv  29053  edgumgr  29081  numedglnl  29090  umgredgnlp  29093  edgusgr  29106  usgruspgrb  29129  uhgr2edg  29154  usgredg2v  29173  ushgredgedgloop  29177  usgr1e  29191  usgrexmplef  29205  subumgredg2  29231  umgrreslem  29251  cusgrexilem2  29388  cusgrexg  29390  fusgrn0degnn0  29446  umgr2v2e  29472  vdiscusgr  29478  rusgr1vtxlem  29534  rgrusgrprc  29536  wlkon2n0  29613  upgrwlkdvdelem  29685  spthonepeq  29701  usgr2wlkneq  29705  iswwlksn  29787  wwlksnon  29800  wwlksn0  29812  wlkiswwlksupgr2  29826  wlknwwlksnbij  29837  wwlksnextbi  29843  wwlksnextfun  29847  wwlksnextinj  29848  wwlksnextbij  29851  2pthon3v  29892  umgr2wlk  29898  rusgrnumwwlkb0  29920  isclwwlkn  29975  clwwlkn1loopb  29991  hashecclwwlkn1  30025  s2elclwwlknon2  30052  uhgr3cyclex  30130  frgrwopreglem4a  30258  frgrwopreglem3  30262  frgrwopreglem5lem  30268  frgrwopreglem5  30269  frgrregorufr0  30272  friendshipgt3  30346  nvz  30617  nmlno0i  30742  norm1exi  31198  pjoc1  31382  pjoc2  31387  pj11  31662  elnlfn  31876  nmlnop0  31946  adjbd1o  32033  strlem1  32198  stcltr1i  32222  2ndimaxp  32592  fnpreimac  32617  indf1ofs  32796  isarchi  33133  ply1dg1rt  33544  minplyval  33690  qtophaus  33810  locfinreflem  33814  rhmpreimacn  33859  isrrext  33976  eulerpartlemsv3  34338  eulerpartlemgvv  34353  ballotlemelo  34465  ballotlemfmpn  34472  ballotlemiex  34479  ballotlemi1  34480  ballotlemii  34481  ballotlemfrcn0  34507  ballotlemirc  34509  bnj229  34873  bnj517  34874  bnj590  34899  bnj1097  34970  bnj1118  34973  bnj1128  34979  bnj1145  34982  f1resfz0f1d  35094  loop1cycl  35117  umgr2cycl  35121  subfacp1lem3  35162  cvmlift3lem5  35303  satffunlem1lem1  35382  satffunlem2lem1  35384  satffunlem2lem2  35386  mthmi  35557  rankeq1o  36147  weiunfr  36443  finxpreclem6  37372  poimirlem13  37615  poimirlem14  37616  poimirlem17  37619  poimirlem18  37620  poimirlem21  37623  poimirlem27  37629  poimirlem28  37630  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  lfl1  39046  lshpkrex  39094  cdleme50rnlem  40521  dochkr1  41455  dochkr1OLDN  41456  lcfrlem28  41547  mapd1o  41625  hdmap1vallem  41774  aks6d1c4  42100  hashnexinjle  42105  sticksstones2  42123  sticksstones3  42124  aks6d1c6lem3  42148  aks6d1c6isolem1  42150  aks6d1c6isolem2  42151  grpods  42170  unitscyglem1  42171  unitscyglem2  42172  unitscyglem3  42173  unitscyglem4  42174  unitscyglem5  42175  diophrw  42748  eldioph3  42755  diophin  42761  eq0rabdioph  42765  eldioph4b  42800  fphpdo  42806  fnwe2lem2  43041  fnwe2lem3  43042  islssfgi  43062  hbt  43120  dgraaval  43134  dgraalem  43135  dgraaub  43138  mpaaeu  43140  mpaaval  43141  mpaalem  43142  rngunsnply  43159  idomsubgmo  43183  proot1mul  43184  cantnfresb  43314  fvelrnbf  44995  wessf1ornlem  45162  sumnnodd  45617  fourierdlem2  46096  fourierdlem3  46097  fcoresf1  47054  uniimafveqt  47341  elsetpreimafvrab  47354  prpair  47461  prproropf1olem1  47463  pairreueq  47470  paireqne  47471  prprspr2  47478  reuprpr  47483  requad2  47583  uhgrimisgrgriclem  47871  clnbgrgrimlem  47874  clnbgrgrim  47875  usgrgrtrirex  47890  stgrusgra  47899  uspgrlimlem1  47928  uspgrlimlem2  47929  grlimgrtri  47936  usgrexmpl1lem  47953  usgrexmpl2lem  47958  gpgusgralem  47984  uspgrsprfo  48037  ply1mulgsumlem2  48277  lindslinindsimp1  48347  snlindsntor  48361  nn0sumshdiglemA  48513  nn0sumshdiglemB  48514  nn0sumshdiglem1  48515  nn0sumshdig  48517  istermc  49173