Theorem fveqeq2 6900

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550

This theorem is referenced by:  fvelimad  6960  dff13f  7260  f1veqaeq  7261  f1elima  7267  fpropnf1  7271  nf1const  7307  oteqimp  8006  fimaproj  8134  suppfnss  8187  suppssfv  8201  tz7.48lem  8455  seqomlem1  8464  seqomlem2  8465  fofinf1o  9345  fipreima  9376  cantnfp1lem3  9697  brttrcl2  9731  ssttrcl  9732  ttrcltr  9733  tcrank  9901  updjudhcoinlf  9949  updjudhcoinrg  9950  pm54.43lem  10017  ackbij1lem18  10254  ackbij1  10255  axcc2  10454  iunfo  10556  grur1  10837  injresinjlem  13778  injresinj  13779  suppssfz  13985  seqid2  14039  hashrabsn01  14358  hashrabsn1  14359  hashimarni  14426  hashbclem  14437  hashbc  14438  hash2exprb  14458  elss2prb  14474  hash2sspr  14475  fi1uzind  14484  brfi1indALT  14487  wrdmap  14522  wrdl1s1  14590  wrdind  14698  wrd2ind  14699  reuccatpfxs1lem  14722  reuccatpfxs1  14723  cshf1  14786  cshw1  14798  wwlktovf  14933  wwlktovf1  14934  wwlktovfo  14935  wrd2f1tovbij  14937  wrdl3s3  14939  abs1m  15308  sumrblem  15683  fsumcvg  15684  summolem2a  15687  incexc2  15810  ntrivcvgfvn0  15871  prodrblem  15899  fprodcvg  15900  prodmolem2a  15904  smupvallem  16451  smu01lem  16453  algfx  16544  iserodd  16797  prmreclem2  16879  prmreclem3  16880  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  hashbcval  16964  ramub1lem1  16988  ramub1lem2  16989  imasleval  17516  eldmcoa  18047  coaval  18050  ghmf1  19193  ghmquskerlem1  19227  orbsta  19257  symgextf1  19369  psgnunilem2  19443  psgnunilem3  19444  psgnunilem4  19445  odeq1  19508  odngen  19525  sylow1lem2  19547  sylow1lem4  19549  sylow1lem5  19550  pgpfi  19553  efgtlen  19674  efgsfo  19687  efgredlemd  19692  efgred  19696  gsummptnn0fzfv  19935  isabvd  20693  abveq0  20699  abvdom  20711  islbs  20954  isobs  21647  cply1mul  22208  mdetunilem1  22507  mdetunilem4  22510  mdetunilem8  22514  mdetunilem9  22515  pmatcoe1fsupp  22596  m2cpminvid2lem  22649  mp2pm2mplem4  22704  2ndci  23345  2ndcsb  23346  2ndcsep  23356  txkgen  23549  nmoeq0  24646  nmoleub3  25039  ivth  25376  ivthle  25378  ivthle2  25379  ovolunlem1  25419  ovolicc2  25444  volivth  25529  mbfinf  25587  itg2splitlem  25671  rollelem  25914  rolle  25915  tdeglem4  25988  tdeglem4OLD  25989  mdeglt  25994  deg1leb  26024  deg1lt  26026  fta1g  26097  ig1peu  26102  ig1pval3  26105  dgrle  26170  0dgrb  26173  dgreq0  26193  fta1lem  26235  fta1  26236  aannenlem1  26256  aannenlem2  26257  aalioulem2  26261  reeff1o  26377  eflogeq  26529  argregt0  26537  argrege0  26538  efopn  26585  asinsinb  26822  acoscosb  26823  atantanb  26849  musum  27116  dchrptlem1  27190  dchrptlem2  27191  lgsquadlem1  27306  nosupcbv  27628  nosupfv  27632  noinfcbv  27643  noinffv  27647  nocvxmin  27704  scutbday  27730  eqscut  27731  scutun12  27736  scutbdaylt  27744  cuteq0  27758  renegscl  28219  istrkgl  28255  mirreu  28461  israg  28494  lmireu  28587  lmieq  28588  gropd  28837  grstructd  28838  umgredg2  28906  umgrbi  28907  umgrnloopv  28912  umgredgprv  28913  edgumgr  28941  numedglnl  28950  umgredgnlp  28953  edgusgr  28966  usgruspgrb  28989  uhgr2edg  29014  usgredg2v  29033  ushgredgedgloop  29037  usgr1e  29051  usgrexmplef  29065  subumgredg2  29091  umgrreslem  29111  cusgrexilem2  29248  cusgrexg  29250  fusgrn0degnn0  29306  umgr2v2e  29332  vdiscusgr  29338  rusgr1vtxlem  29394  rgrusgrprc  29396  wlkon2n0  29473  upgrwlkdvdelem  29543  spthonepeq  29559  usgr2wlkneq  29563  iswwlksn  29642  wwlksnon  29655  wwlksn0  29667  wlkiswwlksupgr2  29681  wlknwwlksnbij  29692  wwlksnextbi  29698  wwlksnextfun  29702  wwlksnextinj  29703  wwlksnextbij  29706  2pthon3v  29747  umgr2wlk  29753  rusgrnumwwlkb0  29775  isclwwlkn  29830  clwwlkn1loopb  29846  hashecclwwlkn1  29880  s2elclwwlknon2  29907  uhgr3cyclex  29985  frgrwopreglem4a  30113  frgrwopreglem3  30117  frgrwopreglem5lem  30123  frgrwopreglem5  30124  frgrregorufr0  30127  friendshipgt3  30201  nvz  30472  nmlno0i  30597  norm1exi  31053  pjoc1  31237  pjoc2  31242  pj11  31517  elnlfn  31731  nmlnop0  31801  adjbd1o  31888  strlem1  32053  stcltr1i  32077  2ndimaxp  32426  fnpreimac  32450  isarchi  32884  ghmqusnsglem1  33123  minplyval  33370  qtophaus  33431  locfinreflem  33435  rhmpreimacn  33480  isrrext  33595  indf1ofs  33639  eulerpartlemsv3  33975  eulerpartlemgvv  33990  ballotlemelo  34101  ballotlemfmpn  34108  ballotlemiex  34115  ballotlemi1  34116  ballotlemii  34117  ballotlemfrcn0  34143  ballotlemirc  34145  bnj229  34509  bnj517  34510  bnj590  34535  bnj1097  34606  bnj1118  34609  bnj1128  34615  bnj1145  34618  f1resfz0f1d  34717  loop1cycl  34741  umgr2cycl  34745  subfacp1lem3  34786  cvmlift3lem5  34927  satffunlem1lem1  35006  satffunlem2lem1  35008  satffunlem2lem2  35010  mthmi  35181  rankeq1o  35761  finxpreclem6  36869  poimirlem13  37100  poimirlem14  37101  poimirlem17  37104  poimirlem18  37105  poimirlem21  37108  poimirlem27  37114  poimirlem28  37115  ovoliunnfl  37129  voliunnfl  37131  volsupnfl  37132  lfl1  38536  lshpkrex  38584  cdleme50rnlem  40011  dochkr1  40945  dochkr1OLDN  40946  lcfrlem28  41037  mapd1o  41115  hdmap1vallem  41264  aks6d1c4  41589  hashnexinjle  41594  sticksstones2  41613  sticksstones3  41614  aks6d1c6lem3  41638  aks6d1c6isolem1  41640  aks6d1c6isolem2  41641  diophrw  42173  eldioph3  42180  diophin  42186  eq0rabdioph  42190  eldioph4b  42225  fphpdo  42231  fnwe2lem2  42469  fnwe2lem3  42470  islssfgi  42490  hbt  42548  dgraaval  42562  dgraalem  42563  dgraaub  42566  mpaaeu  42568  mpaaval  42569  mpaalem  42570  rngunsnply  42591  idomsubgmo  42615  proot1mul  42616  cantnfresb  42747  fvelrnbf  44374  wessf1ornlem  44552  sumnnodd  45012  fourierdlem2  45491  fourierdlem3  45492  fcoresf1  46445  uniimafveqt  46715  elsetpreimafvrab  46728  prpair  46835  prproropf1olem1  46837  pairreueq  46844  paireqne  46845  prprspr2  46852  reuprpr  46857  requad2  46957  uspgrsprfo  47204  ply1mulgsumlem2  47449  lindslinindsimp1  47519  snlindsntor  47533  nn0sumshdiglemA  47686  nn0sumshdiglemB  47687  nn0sumshdiglem1  47688  nn0sumshdig  47690