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 1542  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506

This theorem is referenced by:  fvelimad  6907  dff13f  7210  f1veqaeq  7211  f1elima  7218  fpropnf1  7222  nf1const  7259  oteqimp  7961  fimaproj  8085  suppfnss  8139  suppssfv  8152  tz7.48lem  8380  seqomlem1  8389  seqomlem2  8390  fofinf1o  9242  fipreima  9268  cantnfp1lem3  9601  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  tcrank  9808  updjudhcoinlf  9856  updjudhcoinrg  9857  pm54.43lem  9924  ackbij1lem18  10158  ackbij1  10159  axcc2  10359  iunfo  10461  grur1  10743  injresinjlem  13745  injresinj  13746  suppssfz  13956  seqid2  14010  hashrabsn01  14335  hashrabsn1  14336  hashimarni  14403  hashbclem  14414  hashbc  14415  hash2exprb  14433  elss2prb  14450  hash2sspr  14451  hash3tpde  14455  fi1uzind  14469  brfi1indALT  14472  wrdmap  14508  wrdl1s1  14577  wrdind  14684  wrd2ind  14685  reuccatpfxs1lem  14708  reuccatpfxs1  14709  cshf1  14772  cshw1  14784  wwlktovf  14918  wwlktovf1  14919  wwlktovfo  14920  wrd2f1tovbij  14922  wrdl3s3  14924  abs1m  15298  sumrblem  15673  fsumcvg  15674  summolem2a  15677  incexc2  15803  ntrivcvgfvn0  15864  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  smupvallem  16452  smu01lem  16454  algfx  16549  iserodd  16806  prmreclem2  16888  prmreclem3  16889  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  hashbcval  16973  ramub1lem1  16997  ramub1lem2  16998  imasleval  17505  eldmcoa  18032  coaval  18035  ghmf1  19221  ghmqusnsglem1  19255  ghmquskerlem1  19258  orbsta  19288  symgextf1  19396  psgnunilem2  19470  psgnunilem3  19471  psgnunilem4  19472  odeq1  19535  odngen  19552  sylow1lem2  19574  sylow1lem4  19576  sylow1lem5  19577  pgpfi  19580  efgtlen  19701  efgsfo  19714  efgredlemd  19719  efgred  19723  gsummptnn0fzfv  19962  isabvd  20789  abveq0  20795  abvdom  20807  islbs  21071  isobs  21700  cply1mul  22261  mdetunilem1  22577  mdetunilem4  22580  mdetunilem8  22584  mdetunilem9  22585  pmatcoe1fsupp  22666  m2cpminvid2lem  22719  mp2pm2mplem4  22774  2ndci  23413  2ndcsb  23414  2ndcsep  23424  txkgen  23617  nmoeq0  24701  nmoleub3  25086  ivth  25421  ivthle  25423  ivthle2  25424  ovolunlem1  25464  ovolicc2  25489  volivth  25574  mbfinf  25632  itg2splitlem  25715  rollelem  25956  rolle  25957  tdeglem4  26025  mdeglt  26030  deg1leb  26060  deg1lt  26062  fta1g  26135  ig1peu  26140  ig1pval3  26143  dgrle  26208  0dgrb  26211  dgreq0  26230  fta1lem  26273  fta1  26274  aannenlem1  26294  aannenlem2  26295  aalioulem2  26299  reeff1o  26412  eflogeq  26566  argregt0  26574  argrege0  26575  efopn  26622  asinsinb  26861  acoscosb  26862  atantanb  26888  musum  27154  dchrptlem1  27227  dchrptlem2  27228  lgsquadlem1  27343  nosupcbv  27666  nosupfv  27670  noinfcbv  27681  noinffv  27685  nocvxmin  27747  cutbday  27776  eqcuts  27777  cutsun12  27782  cutbdaylt  27790  cuteq0  27807  negleft  28050  negright  28051  oniso  28263  bdayn0sf1o  28362  dfnns2  28364  znegscl  28384  renegscl  28490  istrkgl  28526  mirreu  28732  israg  28765  lmireu  28858  lmieq  28859  gropd  29100  grstructd  29101  umgredg2  29169  umgrbi  29170  umgrnloopv  29175  umgredgprv  29176  edgumgr  29204  numedglnl  29213  umgredgnlp  29216  edgusgr  29229  usgruspgrb  29252  uhgr2edg  29277  usgredg2v  29296  ushgredgedgloop  29300  usgr1e  29314  usgrexmplef  29328  subumgredg2  29354  umgrreslem  29374  cusgrexilem2  29511  cusgrexg  29513  fusgrn0degnn0  29568  umgr2v2e  29594  vdiscusgr  29600  rusgr1vtxlem  29656  rgrusgrprc  29658  wlkon2n0  29733  upgrwlkdvdelem  29804  spthonepeq  29820  usgr2wlkneq  29824  iswwlksn  29906  wwlksnon  29919  wwlksn0  29931  wlkiswwlksupgr2  29945  wlknwwlksnbij  29956  wwlksnextbi  29962  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextbij  29970  2pthon3v  30011  umgr2wlk  30017  rusgrnumwwlkb0  30042  isclwwlkn  30097  clwwlkn1loopb  30113  hashecclwwlkn1  30147  s2elclwwlknon2  30174  uhgr3cyclex  30252  frgrwopreglem4a  30380  frgrwopreglem3  30384  frgrwopreglem5lem  30390  frgrwopreglem5  30391  frgrregorufr0  30394  friendshipgt3  30468  nvz  30740  nmlno0i  30865  norm1exi  31321  pjoc1  31505  pjoc2  31510  pj11  31785  elnlfn  31999  nmlnop0  32069  adjbd1o  32156  strlem1  32321  stcltr1i  32345  2ndimaxp  32719  fnpreimac  32743  indf1ofs  32926  isarchi  33243  ply1dg1rt  33640  extvfval  33676  esplyfval0  33708  esplymhp  33712  esplyfv1  33713  vieta  33724  minplyval  33849  qtophaus  33980  locfinreflem  33984  rhmpreimacn  34029  isrrext  34144  eulerpartlemsv3  34505  eulerpartlemgvv  34520  ballotlemelo  34632  ballotlemfmpn  34639  ballotlemiex  34646  ballotlemi1  34647  ballotlemii  34648  ballotlemfrcn0  34674  ballotlemirc  34676  bnj229  35026  bnj517  35027  bnj590  35052  bnj1097  35123  bnj1118  35126  bnj1128  35132  bnj1145  35135  f1resfz0f1d  35296  loop1cycl  35319  umgr2cycl  35323  subfacp1lem3  35364  cvmlift3lem5  35505  satffunlem1lem1  35584  satffunlem2lem1  35586  satffunlem2lem2  35588  mthmi  35759  rankeq1o  36353  weiunfr  36649  finxpreclem6  37712  poimirlem13  37954  poimirlem14  37955  poimirlem17  37958  poimirlem18  37959  poimirlem21  37962  poimirlem27  37968  poimirlem28  37969  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  lfl1  39516  lshpkrex  39564  cdleme50rnlem  40990  dochkr1  41924  dochkr1OLDN  41925  lcfrlem28  42016  mapd1o  42094  hdmap1vallem  42243  aks6d1c4  42563  hashnexinjle  42568  sticksstones2  42586  sticksstones3  42587  aks6d1c6lem3  42611  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  unitscyglem5  42638  diophrw  43191  eldioph3  43198  diophin  43204  eq0rabdioph  43208  eldioph4b  43239  fphpdo  43245  fnwe2lem2  43479  fnwe2lem3  43480  islssfgi  43500  hbt  43558  dgraaval  43572  dgraalem  43573  dgraaub  43576  mpaaeu  43578  mpaaval  43579  mpaalem  43580  rngunsnply  43597  idomsubgmo  43621  proot1mul  43622  cantnfresb  43752  fvelrnbf  45449  wessf1ornlem  45615  sumnnodd  46060  fourierdlem2  46537  fourierdlem3  46538  fcoresf1  47517  uniimafveqt  47841  elsetpreimafvrab  47854  prpair  47961  prproropf1olem1  47963  pairreueq  47970  paireqne  47971  prprspr2  47978  reuprpr  47983  requad2  48099  cycldlenngric  48404  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409  clnbgrgrim  48410  usgrgrtrirex  48426  stgrusgra  48435  uspgrlimlem1  48464  uspgrlimlem2  48465  grlimgrtri  48479  usgrexmpl1lem  48497  usgrexmpl2lem  48502  gpgusgralem  48532  gpgprismgr4cyclex  48583  uspgrsprfo  48624  ply1mulgsumlem2  48863  lindslinindsimp1  48933  snlindsntor  48947  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  nn0sumshdig  49099  istermc  49949