Theorem fveqeq2 6899

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

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550

This theorem is referenced by:  fvelimad  6958  dff13f  7257  f1veqaeq  7258  f1elima  7264  fpropnf1  7268  nf1const  7304  oteqimp  7996  fimaproj  8123  suppfnss  8176  suppssfv  8189  tz7.48lem  8443  seqomlem1  8452  seqomlem2  8453  fofinf1o  9329  fipreima  9360  cantnfp1lem3  9677  brttrcl2  9711  ssttrcl  9712  ttrcltr  9713  tcrank  9881  updjudhcoinlf  9929  updjudhcoinrg  9930  pm54.43lem  9997  ackbij1lem18  10234  ackbij1  10235  axcc2  10434  iunfo  10536  grur1  10817  injresinjlem  13756  injresinj  13757  suppssfz  13963  seqid2  14018  hashrabsn01  14337  hashrabsn1  14338  hashimarni  14405  hashbclem  14415  hashbc  14416  hash2exprb  14436  elss2prb  14452  hash2sspr  14453  fi1uzind  14462  brfi1indALT  14465  wrdmap  14500  wrdl1s1  14568  wrdind  14676  wrd2ind  14677  reuccatpfxs1lem  14700  reuccatpfxs1  14701  cshf1  14764  cshw1  14776  wwlktovf  14911  wwlktovf1  14912  wwlktovfo  14913  wrd2f1tovbij  14915  wrdl3s3  14917  abs1m  15286  sumrblem  15661  fsumcvg  15662  summolem2a  15665  incexc2  15788  ntrivcvgfvn0  15849  prodrblem  15877  fprodcvg  15878  prodmolem2a  15882  smupvallem  16428  smu01lem  16430  algfx  16521  iserodd  16772  prmreclem2  16854  prmreclem3  16855  vdwlem2  16919  vdwlem6  16923  vdwlem8  16925  hashbcval  16939  ramub1lem1  16963  ramub1lem2  16964  imasleval  17491  eldmcoa  18019  coaval  18022  ghmf1  19160  orbsta  19218  symgextf1  19330  psgnunilem2  19404  psgnunilem3  19405  psgnunilem4  19406  odeq1  19469  odngen  19486  sylow1lem2  19508  sylow1lem4  19510  sylow1lem5  19511  pgpfi  19514  efgtlen  19635  efgsfo  19648  efgredlemd  19653  efgred  19657  gsummptnn0fzfv  19896  isabvd  20571  abveq0  20577  abvdom  20589  islbs  20831  isobs  21494  cply1mul  22038  mdetunilem1  22334  mdetunilem4  22337  mdetunilem8  22341  mdetunilem9  22342  pmatcoe1fsupp  22423  m2cpminvid2lem  22476  mp2pm2mplem4  22531  2ndci  23172  2ndcsb  23173  2ndcsep  23183  txkgen  23376  nmoeq0  24473  nmoleub3  24866  ivth  25203  ivthle  25205  ivthle2  25206  ovolunlem1  25246  ovolicc2  25271  volivth  25356  mbfinf  25414  itg2splitlem  25498  rollelem  25741  rolle  25742  tdeglem4  25812  tdeglem4OLD  25813  mdeglt  25818  deg1leb  25848  deg1lt  25850  fta1g  25920  ig1peu  25924  ig1pval3  25927  dgrle  25992  0dgrb  25995  dgreq0  26015  fta1lem  26056  fta1  26057  aannenlem1  26077  aannenlem2  26078  aalioulem2  26082  reeff1o  26195  eflogeq  26346  argregt0  26354  argrege0  26355  efopn  26402  asinsinb  26638  acoscosb  26639  atantanb  26665  musum  26931  dchrptlem1  27003  dchrptlem2  27004  lgsquadlem1  27119  nosupcbv  27441  nosupfv  27445  noinfcbv  27456  noinffv  27460  nocvxmin  27516  scutbday  27542  eqscut  27543  scutun12  27548  scutbdaylt  27556  cuteq0  27570  istrkgl  27976  mirreu  28182  israg  28215  lmireu  28308  lmieq  28309  gropd  28558  grstructd  28559  umgredg2  28627  umgrbi  28628  umgrnloopv  28633  umgredgprv  28634  edgumgr  28662  numedglnl  28671  umgredgnlp  28674  edgusgr  28687  usgruspgrb  28708  uhgr2edg  28732  usgredg2v  28751  ushgredgedgloop  28755  usgr1e  28769  usgrexmplef  28783  subumgredg2  28809  umgrreslem  28829  cusgrexilem2  28966  cusgrexg  28968  fusgrn0degnn0  29023  umgr2v2e  29049  vdiscusgr  29055  rusgr1vtxlem  29111  rgrusgrprc  29113  wlkon2n0  29190  upgrwlkdvdelem  29260  spthonepeq  29276  usgr2wlkneq  29280  iswwlksn  29359  wwlksnon  29372  wwlksn0  29384  wlkiswwlksupgr2  29398  wlknwwlksnbij  29409  wwlksnextbi  29415  wwlksnextfun  29419  wwlksnextinj  29420  wwlksnextbij  29423  2pthon3v  29464  umgr2wlk  29470  rusgrnumwwlkb0  29492  isclwwlkn  29547  clwwlkn1loopb  29563  hashecclwwlkn1  29597  s2elclwwlknon2  29624  uhgr3cyclex  29702  frgrwopreglem4a  29830  frgrwopreglem3  29834  frgrwopreglem5lem  29840  frgrwopreglem5  29841  frgrregorufr0  29844  friendshipgt3  29918  nvz  30189  nmlno0i  30314  norm1exi  30770  pjoc1  30954  pjoc2  30959  pj11  31234  elnlfn  31448  nmlnop0  31518  adjbd1o  31605  strlem1  31770  stcltr1i  31794  2ndimaxp  32139  fnpreimac  32163  isarchi  32598  ghmquskerlem1  32802  minplyval  33055  qtophaus  33114  locfinreflem  33118  rhmpreimacn  33163  isrrext  33278  indf1ofs  33322  eulerpartlemsv3  33658  eulerpartlemgvv  33673  ballotlemelo  33784  ballotlemfmpn  33791  ballotlemiex  33798  ballotlemi1  33799  ballotlemii  33800  ballotlemfrcn0  33826  ballotlemirc  33828  bnj229  34193  bnj517  34194  bnj590  34219  bnj1097  34290  bnj1118  34293  bnj1128  34299  bnj1145  34302  f1resfz0f1d  34401  loop1cycl  34426  umgr2cycl  34430  subfacp1lem3  34471  cvmlift3lem5  34612  satffunlem1lem1  34691  satffunlem2lem1  34693  satffunlem2lem2  34695  mthmi  34866  rankeq1o  35447  finxpreclem6  36580  poimirlem13  36804  poimirlem14  36805  poimirlem17  36808  poimirlem18  36809  poimirlem21  36812  poimirlem27  36818  poimirlem28  36819  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  lfl1  38243  lshpkrex  38291  cdleme50rnlem  39718  dochkr1  40652  dochkr1OLDN  40653  lcfrlem28  40744  mapd1o  40822  hdmap1vallem  40971  sticksstones2  41269  sticksstones3  41270  diophrw  41799  eldioph3  41806  diophin  41812  eq0rabdioph  41816  eldioph4b  41851  fphpdo  41857  fnwe2lem2  42095  fnwe2lem3  42096  islssfgi  42116  hbt  42174  dgraaval  42188  dgraalem  42189  dgraaub  42192  mpaaeu  42194  mpaaval  42195  mpaalem  42196  rngunsnply  42217  idomsubgmo  42242  proot1mul  42243  cantnfresb  42376  fvelrnbf  44004  wessf1ornlem  44182  sumnnodd  44644  fourierdlem2  45123  fourierdlem3  45124  fcoresf1  46077  uniimafveqt  46347  elsetpreimafvrab  46360  prpair  46467  prproropf1olem1  46469  pairreueq  46476  paireqne  46477  prprspr2  46484  reuprpr  46489  requad2  46589  uspgrsprfo  46824  ply1mulgsumlem2  47155  lindslinindsimp1  47225  snlindsntor  47239  nn0sumshdiglemA  47392  nn0sumshdiglemB  47393  nn0sumshdiglem1  47394  nn0sumshdig  47396