Theorem fveqeq2 6884

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538

This theorem is referenced by:  fvelimad  6945  dff13f  7247  f1veqaeq  7248  f1elima  7255  fpropnf1  7259  nf1const  7296  oteqimp  8005  fimaproj  8132  suppfnss  8186  suppssfv  8199  tz7.48lem  8453  seqomlem1  8462  seqomlem2  8463  fofinf1o  9342  fipreima  9368  cantnfp1lem3  9692  brttrcl2  9726  ssttrcl  9727  ttrcltr  9728  tcrank  9896  updjudhcoinlf  9944  updjudhcoinrg  9945  pm54.43lem  10012  ackbij1lem18  10248  ackbij1  10249  axcc2  10449  iunfo  10551  grur1  10832  injresinjlem  13801  injresinj  13802  suppssfz  14010  seqid2  14064  hashrabsn01  14389  hashrabsn1  14390  hashimarni  14457  hashbclem  14468  hashbc  14469  hash2exprb  14487  elss2prb  14504  hash2sspr  14505  hash3tpde  14509  fi1uzind  14523  brfi1indALT  14526  wrdmap  14562  wrdl1s1  14630  wrdind  14738  wrd2ind  14739  reuccatpfxs1lem  14762  reuccatpfxs1  14763  cshf1  14826  cshw1  14838  wwlktovf  14973  wwlktovf1  14974  wwlktovfo  14975  wrd2f1tovbij  14977  wrdl3s3  14979  abs1m  15352  sumrblem  15725  fsumcvg  15726  summolem2a  15729  incexc2  15852  ntrivcvgfvn0  15913  prodrblem  15943  fprodcvg  15944  prodmolem2a  15948  smupvallem  16500  smu01lem  16502  algfx  16597  iserodd  16853  prmreclem2  16935  prmreclem3  16936  vdwlem2  17000  vdwlem6  17004  vdwlem8  17006  hashbcval  17020  ramub1lem1  17044  ramub1lem2  17045  imasleval  17553  eldmcoa  18076  coaval  18079  ghmf1  19227  ghmqusnsglem1  19261  ghmquskerlem1  19264  orbsta  19294  symgextf1  19400  psgnunilem2  19474  psgnunilem3  19475  psgnunilem4  19476  odeq1  19539  odngen  19556  sylow1lem2  19578  sylow1lem4  19580  sylow1lem5  19581  pgpfi  19584  efgtlen  19705  efgsfo  19718  efgredlemd  19723  efgred  19727  gsummptnn0fzfv  19966  isabvd  20770  abveq0  20776  abvdom  20788  islbs  21032  isobs  21678  cply1mul  22232  mdetunilem1  22548  mdetunilem4  22551  mdetunilem8  22555  mdetunilem9  22556  pmatcoe1fsupp  22637  m2cpminvid2lem  22690  mp2pm2mplem4  22745  2ndci  23384  2ndcsb  23385  2ndcsep  23395  txkgen  23588  nmoeq0  24673  nmoleub3  25068  ivth  25405  ivthle  25407  ivthle2  25408  ovolunlem1  25448  ovolicc2  25473  volivth  25558  mbfinf  25616  itg2splitlem  25699  rollelem  25943  rolle  25944  tdeglem4  26015  mdeglt  26020  deg1leb  26050  deg1lt  26052  fta1g  26125  ig1peu  26130  ig1pval3  26133  dgrle  26198  0dgrb  26201  dgreq0  26221  fta1lem  26265  fta1  26266  aannenlem1  26286  aannenlem2  26287  aalioulem2  26291  reeff1o  26407  eflogeq  26561  argregt0  26569  argrege0  26570  efopn  26617  asinsinb  26857  acoscosb  26858  atantanb  26884  musum  27151  dchrptlem1  27225  dchrptlem2  27226  lgsquadlem1  27341  nosupcbv  27664  nosupfv  27668  noinfcbv  27679  noinffv  27683  nocvxmin  27740  scutbday  27766  eqscut  27767  scutun12  27772  scutbdaylt  27780  cuteq0  27794  dfnns2  28279  znegscl  28295  renegscl  28347  istrkgl  28383  mirreu  28589  israg  28622  lmireu  28715  lmieq  28716  gropd  28956  grstructd  28957  umgredg2  29025  umgrbi  29026  umgrnloopv  29031  umgredgprv  29032  edgumgr  29060  numedglnl  29069  umgredgnlp  29072  edgusgr  29085  usgruspgrb  29108  uhgr2edg  29133  usgredg2v  29152  ushgredgedgloop  29156  usgr1e  29170  usgrexmplef  29184  subumgredg2  29210  umgrreslem  29230  cusgrexilem2  29367  cusgrexg  29369  fusgrn0degnn0  29425  umgr2v2e  29451  vdiscusgr  29457  rusgr1vtxlem  29513  rgrusgrprc  29515  wlkon2n0  29592  upgrwlkdvdelem  29664  spthonepeq  29680  usgr2wlkneq  29684  iswwlksn  29766  wwlksnon  29779  wwlksn0  29791  wlkiswwlksupgr2  29805  wlknwwlksnbij  29816  wwlksnextbi  29822  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextbij  29830  2pthon3v  29871  umgr2wlk  29877  rusgrnumwwlkb0  29899  isclwwlkn  29954  clwwlkn1loopb  29970  hashecclwwlkn1  30004  s2elclwwlknon2  30031  uhgr3cyclex  30109  frgrwopreglem4a  30237  frgrwopreglem3  30241  frgrwopreglem5lem  30247  frgrwopreglem5  30248  frgrregorufr0  30251  friendshipgt3  30325  nvz  30596  nmlno0i  30721  norm1exi  31177  pjoc1  31361  pjoc2  31366  pj11  31641  elnlfn  31855  nmlnop0  31925  adjbd1o  32012  strlem1  32177  stcltr1i  32201  2ndimaxp  32570  fnpreimac  32595  indf1ofs  32789  isarchi  33126  ply1dg1rt  33538  minplyval  33685  qtophaus  33813  locfinreflem  33817  rhmpreimacn  33862  isrrext  33977  eulerpartlemsv3  34339  eulerpartlemgvv  34354  ballotlemelo  34466  ballotlemfmpn  34473  ballotlemiex  34480  ballotlemi1  34481  ballotlemii  34482  ballotlemfrcn0  34508  ballotlemirc  34510  bnj229  34861  bnj517  34862  bnj590  34887  bnj1097  34958  bnj1118  34961  bnj1128  34967  bnj1145  34970  f1resfz0f1d  35082  loop1cycl  35105  umgr2cycl  35109  subfacp1lem3  35150  cvmlift3lem5  35291  satffunlem1lem1  35370  satffunlem2lem1  35372  satffunlem2lem2  35374  mthmi  35545  rankeq1o  36135  weiunfr  36431  finxpreclem6  37360  poimirlem13  37603  poimirlem14  37604  poimirlem17  37607  poimirlem18  37608  poimirlem21  37611  poimirlem27  37617  poimirlem28  37618  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  lfl1  39034  lshpkrex  39082  cdleme50rnlem  40509  dochkr1  41443  dochkr1OLDN  41444  lcfrlem28  41535  mapd1o  41613  hdmap1vallem  41762  aks6d1c4  42083  hashnexinjle  42088  sticksstones2  42106  sticksstones3  42107  aks6d1c6lem3  42131  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  grpods  42153  unitscyglem1  42154  unitscyglem2  42155  unitscyglem3  42156  unitscyglem4  42157  unitscyglem5  42158  diophrw  42729  eldioph3  42736  diophin  42742  eq0rabdioph  42746  eldioph4b  42781  fphpdo  42787  fnwe2lem2  43022  fnwe2lem3  43023  islssfgi  43043  hbt  43101  dgraaval  43115  dgraalem  43116  dgraaub  43119  mpaaeu  43121  mpaaval  43122  mpaalem  43123  rngunsnply  43140  idomsubgmo  43164  proot1mul  43165  cantnfresb  43295  fvelrnbf  44990  wessf1ornlem  45157  sumnnodd  45607  fourierdlem2  46086  fourierdlem3  46087  fcoresf1  47046  uniimafveqt  47343  elsetpreimafvrab  47356  prpair  47463  prproropf1olem1  47465  pairreueq  47472  paireqne  47473  prprspr2  47480  reuprpr  47485  requad2  47585  cycldlenngric  47889  uhgrimisgrgriclem  47891  clnbgrgrimlem  47894  clnbgrgrim  47895  usgrgrtrirex  47910  stgrusgra  47919  uspgrlimlem1  47948  uspgrlimlem2  47949  grlimgrtri  47956  usgrexmpl1lem  47973  usgrexmpl2lem  47978  gpgusgralem  48008  gpgprismgr4cyclex  48054  uspgrsprfo  48071  ply1mulgsumlem2  48311  lindslinindsimp1  48381  snlindsntor  48395  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdiglem1  48549  nn0sumshdig  48551  istermc  49308