Theorem fveqeq2 6765

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by:  fvelimad  6818  dff13f  7110  f1veqaeq  7111  f1elima  7117  fpropnf1  7121  nf1const  7156  oteqimp  7823  fimaproj  7947  suppfnss  7976  suppssfv  7989  tz7.48lem  8242  seqomlem1  8251  seqomlem2  8252  fofinf1o  9024  fipreima  9055  cantnfp1lem3  9368  trpred0  9410  tcrank  9573  updjudhcoinlf  9621  updjudhcoinrg  9622  pm54.43lem  9689  ackbij1lem18  9924  ackbij1  9925  axcc2  10124  iunfo  10226  grur1  10507  injresinjlem  13435  injresinj  13436  suppssfz  13642  seqid2  13697  hashrabsn01  14016  hashrabsn1  14017  hashimarni  14084  hashbclem  14092  hashbc  14093  hash2exprb  14113  elss2prb  14129  hash2sspr  14130  fi1uzind  14139  brfi1indALT  14142  wrdmap  14177  wrdl1s1  14247  wrdind  14363  wrd2ind  14364  reuccatpfxs1lem  14387  reuccatpfxs1  14388  cshf1  14451  cshw1  14463  wwlktovf  14599  wwlktovf1  14600  wwlktovfo  14601  wrd2f1tovbij  14603  wrdl3s3  14605  abs1m  14975  sumrblem  15351  fsumcvg  15352  summolem2a  15355  incexc2  15478  ntrivcvgfvn0  15539  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  smupvallem  16118  smu01lem  16120  algfx  16213  iserodd  16464  prmreclem2  16546  prmreclem3  16547  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  hashbcval  16631  ramub1lem1  16655  ramub1lem2  16656  imasleval  17169  eldmcoa  17696  coaval  17699  ghmf1  18778  orbsta  18834  symgextf1  18944  psgnunilem2  19018  psgnunilem3  19019  psgnunilem4  19020  odeq1  19082  odngen  19097  sylow1lem2  19119  sylow1lem4  19121  sylow1lem5  19122  pgpfi  19125  efgtlen  19247  efgsfo  19260  efgredlemd  19265  efgred  19269  gsummptnn0fzfv  19503  isabvd  19995  abveq0  20001  abvdom  20013  islbs  20253  isobs  20837  cply1mul  21375  mdetunilem1  21669  mdetunilem4  21672  mdetunilem8  21676  mdetunilem9  21677  pmatcoe1fsupp  21758  m2cpminvid2lem  21811  mp2pm2mplem4  21866  2ndci  22507  2ndcsb  22508  2ndcsep  22518  txkgen  22711  nmoeq0  23806  nmoleub3  24188  ivth  24523  ivthle  24525  ivthle2  24526  ovolunlem1  24566  ovolicc2  24591  volivth  24676  mbfinf  24734  itg2splitlem  24818  rollelem  25058  rolle  25059  tdeglem4  25129  tdeglem4OLD  25130  mdeglt  25135  deg1leb  25165  deg1lt  25167  fta1g  25237  ig1peu  25241  ig1pval3  25244  dgrle  25309  0dgrb  25312  dgreq0  25331  fta1lem  25372  fta1  25373  aannenlem1  25393  aannenlem2  25394  aalioulem2  25398  reeff1o  25511  eflogeq  25662  argregt0  25670  argrege0  25671  efopn  25718  asinsinb  25952  acoscosb  25953  atantanb  25979  musum  26245  dchrptlem1  26317  dchrptlem2  26318  lgsquadlem1  26433  istrkgl  26723  mirreu  26929  israg  26962  lmireu  27055  lmieq  27056  gropd  27304  grstructd  27305  umgredg2  27373  umgrbi  27374  umgrnloopv  27379  umgredgprv  27380  edgumgr  27408  numedglnl  27417  umgredgnlp  27420  edgusgr  27433  usgruspgrb  27454  uhgr2edg  27478  usgredg2v  27497  ushgredgedgloop  27501  usgr1e  27515  usgrexmplef  27529  subumgredg2  27555  umgrreslem  27575  cusgrexilem2  27712  cusgrexg  27714  fusgrn0degnn0  27769  umgr2v2e  27795  vdiscusgr  27801  rusgr1vtxlem  27857  rgrusgrprc  27859  wlkon2n0  27936  upgrwlkdvdelem  28005  spthonepeq  28021  usgr2wlkneq  28025  iswwlksn  28104  wwlksnon  28117  wwlksn0  28129  wlkiswwlksupgr2  28143  wlknwwlksnbij  28154  wwlksnextbi  28160  wwlksnextfun  28164  wwlksnextinj  28165  wwlksnextbij  28168  2pthon3v  28209  umgr2wlk  28215  rusgrnumwwlkb0  28237  isclwwlkn  28292  clwwlkn1loopb  28308  hashecclwwlkn1  28342  s2elclwwlknon2  28369  uhgr3cyclex  28447  frgrwopreglem4a  28575  frgrwopreglem3  28579  frgrwopreglem5lem  28585  frgrwopreglem5  28586  frgrregorufr0  28589  friendshipgt3  28663  nvz  28932  nmlno0i  29057  norm1exi  29513  pjoc1  29697  pjoc2  29702  pj11  29977  elnlfn  30191  nmlnop0  30261  adjbd1o  30348  strlem1  30513  stcltr1i  30537  2ndimaxp  30885  fnpreimac  30910  isarchi  31338  qtophaus  31688  locfinreflem  31692  rhmpreimacn  31737  isrrext  31850  indf1ofs  31894  eulerpartlemsv3  32228  eulerpartlemgvv  32243  ballotlemelo  32354  ballotlemfmpn  32361  ballotlemiex  32368  ballotlemi1  32369  ballotlemii  32370  ballotlemfrcn0  32396  ballotlemirc  32398  bnj229  32764  bnj517  32765  bnj590  32790  bnj1097  32861  bnj1118  32864  bnj1128  32870  bnj1145  32873  f1resfz0f1d  32972  loop1cycl  32999  umgr2cycl  33003  subfacp1lem3  33044  cvmlift3lem5  33185  satffunlem1lem1  33264  satffunlem2lem1  33266  satffunlem2lem2  33268  mthmi  33439  brttrcl2  33700  ssttrcl  33701  ttrcltr  33702  nosupcbv  33832  nosupfv  33836  noinfcbv  33847  noinffv  33851  nocvxmin  33900  scutbday  33925  eqscut  33926  scutun12  33931  scutbdaylt  33939  rankeq1o  34400  finxpreclem6  35494  poimirlem13  35717  poimirlem14  35718  poimirlem17  35721  poimirlem18  35722  poimirlem21  35725  poimirlem27  35731  poimirlem28  35732  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  lfl1  37011  lshpkrex  37059  cdleme50rnlem  38485  dochkr1  39419  dochkr1OLDN  39420  lcfrlem28  39511  mapd1o  39589  hdmap1vallem  39738  sticksstones2  40031  sticksstones3  40032  diophrw  40497  eldioph3  40504  diophin  40510  eq0rabdioph  40514  eldioph4b  40549  fphpdo  40555  fnwe2lem2  40792  fnwe2lem3  40793  islssfgi  40813  hbt  40871  dgraaval  40885  dgraalem  40886  dgraaub  40889  mpaaeu  40891  mpaaval  40892  mpaalem  40893  rngunsnply  40914  idomsubgmo  40939  proot1mul  40940  fvelrnbf  42450  wessf1ornlem  42611  sumnnodd  43061  fourierdlem2  43540  fourierdlem3  43541  fcoresf1  44450  uniimafveqt  44721  elsetpreimafvrab  44734  prpair  44841  prproropf1olem1  44843  pairreueq  44850  paireqne  44851  prprspr2  44858  reuprpr  44863  requad2  44963  uspgrsprfo  45198  ply1mulgsumlem2  45616  lindslinindsimp1  45686  snlindsntor  45700  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855  nn0sumshdig  45857