Theorem fveqeq2 6905

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fveqeq2d 6904	1 ⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ‘cfv 6547

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555

This theorem is used by:  fvelimad  6963  dff13f  7269  f1veqaeq  7270  f1elima  7277  fpropnf1  7281  nf1const  7322  oteqimp  8030  fnwe2lem3  8160  fnwe2lem4  8161  fimaproj  8165  suppfnss  8220  suppssfv  8233  tz7.48lemOLD  8465  seqomlem1  8474  seqomlem2  8475  fofinf1o  9335  fipreima  9361  cantnfp1lem3  9694  brttrcl2  9728  ssttrcl  9729  ttrcltr  9730  tcrank  9914  updjudhcoinlf  10026  updjudhcoinrg  10027  pm54.43lem  10094  ackbij1lem18  10327  ackbij1  10328  axcc2  10528  iunfo  10636  grur1  10918  injresinjlem  13938  injresinj  13939  f1resfz0f1d  13940  suppssfz  14150  seqid2  14204  hashrabsn01  14530  hashrabsn1  14531  hashimarni  14599  hashbclem  14610  hashbc  14611  hash2exprb  14629  elss2prb  14646  hash2sspr  14647  hash3tpde  14651  fi1uzind  14665  brfi1indALT  14668  wrdmap  14704  wrdl1s1  14776  wrdind  14885  wrd2ind  14886  reuccatpfxs1lem  14909  reuccatpfxs1  14910  cshf1  14975  cshw1  14987  wwlktovf  15124  wwlktovf1  15125  wwlktovfo  15126  wrd2f1tovbij  15128  wrdl3s3  15130  abs1m  15518  sumrblem  15892  fsumcvg  15893  summolem2a  15896  incexc2  16022  ntrivcvgfvn0  16083  prodrblem  16111  fprodcvg  16112  prodmolem2a  16116  smupvallem  16668  smu01lem  16670  algfx  16770  iserodd  17028  prmreclem2  17110  prmreclem3  17111  vdwlem2  17175  vdwlem6  17179  vdwlem8  17181  hashbcval  17195  ramub1lem1  17219  ramub1lem2  17220  imasleval  17728  eldmcoa  18255  coaval  18258  ghmf1  19475  ghmqusnsglem1  19509  ghmquskerlem1  19512  orbsta  19542  symgextf1  19650  psgnunilem2  19724  psgnunilem3  19725  psgnunilem4  19726  odeq1  19789  odngen  19806  sylow1lem2  19828  sylow1lem4  19830  sylow1lem5  19831  pgpfi  19834  efgtlen  19955  efgsfo  19968  efgredlemd  19973  efgred  19977  gsummptnn0fzfv  20216  isabvd  21084  abveq0  21090  abvdom  21102  islbs  21366  isobs  22041  cply1mul  22629  mdetunilem1  22942  mdetunilem4  22945  mdetunilem8  22949  mdetunilem9  22950  pmatcoe1fsupp  23034  m2cpminvid2lem  23087  mp2pm2mplem4  23142  2ndci  23781  2ndcsb  23782  2ndcsep  23793  txkgen  23986  nmoeq0  25070  nmoleub3  25455  ivth  25790  ivthle  25792  ivthle2  25793  ovolunlem1  25833  ovolicc2  25858  volivth  25943  mbfinf  26001  itg2splitlem  26084  rollelem  26324  rolle  26325  tdeglem4  26393  mdeglt  26398  deg1leb  26428  deg1lt  26430  fta1g  26503  ig1peu  26508  ig1pval3  26511  dgrle  26577  0dgrb  26580  dgreq0  26599  fta1lem  26643  fta1  26644  rnplynfin  26645  plyconz  26646  aannenlem1  26670  aannenlem2  26671  aalioulem2  26675  reeff1o  26789  eflogeq  26945  argregt0  26953  argrege0  26954  efopn  27001  asinsinb  27240  acoscosb  27241  atantanb  27267  musum  27533  dchrptlem1  27606  dchrptlem2  27607  lgsquadlem1  27722  nosupcbv  28074  nosupfv  28078  noinfcbv  28089  noinffv  28093  nocvxmin  28156  cutbday  28185  eqcuts  28186  cutsun12  28191  cutbdaylt  28199  cuteq0  28216  negleft  28459  negright  28460  oniso  28672  bdayn0sf1o  28771  dfnns2  28773  znegscl  28793  renegscl  28899  istrkgl  28935  mirreu  29151  israg  29187  lmireu  29310  lmieq  29311  gropd  29624  grstructd  29625  umgredg2  29693  umgrbi  29694  umgrnloopv  29699  umgredgprv  29700  edgumgr  29728  numedglnl  29737  umgredgnlp  29740  edgusgr  29756  usgruspgrb  29779  uhgr2edg  29804  usgredg2v  29823  ushgredgedgloop  29827  usgr1e  29841  usgrexmplef  29855  subumgredg2  29881  umgrreslem  29901  cusgrexilem2  30038  cusgrexg  30040  fusgrn0degnn0  30095  umgr2v2e  30121  vdiscusgr  30127  rusgr1vtxlem  30183  rgrusgrprc  30185  wlkon2n0  30260  upgrwlkdvdelem  30337  spthonepeq  30353  usgr2wlkneq  30357  iswwlksn  30442  wwlksnon  30455  wwlksn0  30467  wlkiswwlksupgr2  30481  wlknwwlksnbij  30492  wwlksnextbi  30498  wwlksnextfun  30502  wwlksnextinj  30503  wwlksnextbij  30506  2pthon3v  30547  umgr2wlk  30553  rusgrnumwwlkb0  30578  isclwwlkn  30633  clwwlkn1loopb  30649  hashecclwwlkn1  30683  s2elclwwlknon2  30710  loop1cycl  30759  umgr2cycl  30762  uhgr3cyclex  30798  frgrwopreglem4a  30926  frgrwopreglem3  30930  frgrwopreglem5lem  30936  frgrwopreglem5  30937  frgrregorufr0  30940  friendshipgt3  31014  nvz  31286  nmlno0i  31411  norm1exi  31867  pjoc1  32051  pjoc2  32056  pj11  32331  elnlfn  32545  nmlnop0  32615  adjbd1o  32702  strlem1  32867  stcltr1i  32891  2ndimaxp  33297  fnpreimac  33321  indf1ofs  33489  isarchi  33799  ply1dg1rt  34168  extvfval  34220  esplyfval0  34252  esplymhp  34256  esplyfv1  34257  vieta  34268  minplyval  34393  qtophaus  34524  locfinreflem  34528  rhmpreimacn  34573  isrrext  34688  eulerpartlemsv3  35049  eulerpartlemgvv  35064  ballotlemelo  35176  ballotlemfmpn  35183  ballotlemiex  35190  ballotlemi1  35191  ballotlemii  35192  ballotlemfrcn0  35218  ballotlemirc  35220  bnj229  35570  bnj517  35571  bnj590  35596  bnj1097  35667  bnj1118  35670  bnj1128  35676  bnj1145  35679  werankwe  35803  werankwe2  35804  elscott2  35810  elscottrank  35811  acwer1prc  35834  kardeng  35899  vonf1oonfo  36006  subfacp1lem3  36071  cvmlift3lem5  36212  satffunlem1lem1  36291  satffunlem2lem1  36293  satffunlem2lem2  36295  mthmi  36466  rankeq1o  37062  weiunfr  37385  finxpreclem6  38462  poimirlem13  38694  poimirlem14  38695  poimirlem17  38698  poimirlem18  38699  poimirlem21  38702  poimirlem27  38708  poimirlem28  38709  ovoliunnfl  38723  voliunnfl  38725  volsupnfl  38726  lfl1  40270  lshpkrex  40318  cdleme50rnlem  41744  dochkr1  42678  dochkr1OLDN  42679  lcfrlem28  42770  mapd1o  42848  hdmap1vallem  42997  aks6d1c4  43317  hashnexinjle  43322  sticksstones2  43340  sticksstones3  43341  aks6d1c6lem3  43365  aks6d1c6isolem1  43367  aks6d1c6isolem2  43368  grpods  43387  unitscyglem1  43388  unitscyglem2  43389  unitscyglem3  43390  unitscyglem4  43391  unitscyglem5  43392  prjspnnorm  43804  diophrw  43913  eldioph3  43920  diophin  43926  eq0rabdioph  43930  eldioph4b  43961  fphpdo  43967  islssfgi  44217  hbt  44275  dgraaval  44289  dgraalem  44290  dgraaub  44293  mpaaeu  44295  mpaaval  44296  mpaalem  44297  rngunsnply  44314  idomsubgmo  44338  proot1mul  44339  cantnfresb  44469  fvelrnbf  46177  wessf1ornlem  46342  sumnnodd  46784  fourierdlem2  47261  fourierdlem3  47262  fcoresf1  48281  uniimafveqt  48605  elsetpreimafvrab  48618  prpair  48725  prproropf1olem1  48727  pairreueq  48734  paireqne  48735  prprspr2  48742  reuprpr  48747  requad2  48863  cycldlenngric  49168  uhgrimisgrgriclem  49170  clnbgrgrimlem  49173  clnbgrgrim  49174  usgrgrtrirex  49190  stgrusgra  49199  uspgrlimlem1  49228  uspgrlimlem2  49229  grlimgrtri  49243  usgrexmpl1lem  49261  usgrexmpl2lem  49266  gpgusgralem  49296  gpgprismgr4cyclex  49347  uspgrsprfo  49388  ply1mulgsumlem2  49641  lindslinindsimp1  49711  snlindsntor  49725  nn0sumshdiglemA  49873  nn0sumshdiglemB  49874  nn0sumshdiglem1  49875  nn0sumshdig  49877  istermc  50751