Theorem fveqeq2 6654

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ‘cfv 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332

This theorem is referenced by:  fvelimad  6707  dff13f  6992  f1veqaeq  6993  f1elima  6999  fpropnf1  7003  nf1const  7038  oteqimp  7690  fimaproj  7812  suppfnss  7838  suppssfv  7849  tz7.48lem  8060  seqomlem1  8069  seqomlem2  8070  fofinf1o  8783  fipreima  8814  cantnfp1lem3  9127  tcrank  9297  updjudhcoinlf  9345  updjudhcoinrg  9346  pm54.43lem  9413  ackbij1lem18  9648  ackbij1  9649  axcc2  9848  iunfo  9950  grur1  10231  injresinjlem  13152  injresinj  13153  suppssfz  13357  seqid2  13412  hashrabsn01  13730  hashrabsn1  13731  hashimarni  13798  hashbclem  13806  hashbc  13807  hash2exprb  13825  elss2prb  13841  hash2sspr  13842  fi1uzind  13851  brfi1indALT  13854  wrdmap  13889  wrdl1s1  13959  wrdind  14075  wrd2ind  14076  reuccatpfxs1lem  14099  reuccatpfxs1  14100  cshf1  14163  cshw1  14175  wwlktovf  14311  wwlktovf1  14312  wwlktovfo  14313  wrd2f1tovbij  14315  wrdl3s3  14317  abs1m  14687  sumrblem  15060  fsumcvg  15061  summolem2a  15064  incexc2  15185  ntrivcvgfvn0  15247  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  smupvallem  15822  smu01lem  15824  algfx  15914  iserodd  16162  prmreclem2  16243  prmreclem3  16244  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  hashbcval  16328  ramub1lem1  16352  ramub1lem2  16353  imasleval  16806  eldmcoa  17317  coaval  17320  ghmf1  18379  orbsta  18435  symgextf1  18541  psgnunilem2  18615  psgnunilem3  18616  psgnunilem4  18617  odeq1  18679  odngen  18694  sylow1lem2  18716  sylow1lem4  18718  sylow1lem5  18719  pgpfi  18722  efgtlen  18844  efgsfo  18857  efgredlemd  18862  efgred  18866  gsummptnn0fzfv  19100  isabvd  19584  abveq0  19590  abvdom  19602  islbs  19841  isobs  20409  cply1mul  20923  mdetunilem1  21217  mdetunilem4  21220  mdetunilem8  21224  mdetunilem9  21225  pmatcoe1fsupp  21306  m2cpminvid2lem  21359  mp2pm2mplem4  21414  2ndci  22053  2ndcsb  22054  2ndcsep  22064  txkgen  22257  nmoeq0  23342  nmoleub3  23724  ivth  24058  ivthle  24060  ivthle2  24061  ovolunlem1  24101  ovolicc2  24126  volivth  24211  mbfinf  24269  itg2splitlem  24352  rollelem  24592  rolle  24593  tdeglem4  24661  mdeglt  24666  deg1leb  24696  deg1lt  24698  fta1g  24768  ig1peu  24772  ig1pval3  24775  dgrle  24840  0dgrb  24843  dgreq0  24862  fta1lem  24903  fta1  24904  aannenlem1  24924  aannenlem2  24925  aalioulem2  24929  reeff1o  25042  eflogeq  25193  argregt0  25201  argrege0  25202  efopn  25249  asinsinb  25483  acoscosb  25484  atantanb  25510  musum  25776  dchrptlem1  25848  dchrptlem2  25849  lgsquadlem1  25964  istrkgl  26252  mirreu  26458  israg  26491  lmireu  26584  lmieq  26585  gropd  26824  grstructd  26825  umgredg2  26893  umgrbi  26894  umgrnloopv  26899  umgredgprv  26900  edgumgr  26928  numedglnl  26937  umgredgnlp  26940  edgusgr  26953  usgruspgrb  26974  uhgr2edg  26998  usgredg2v  27017  ushgredgedgloop  27021  usgr1e  27035  usgrexmplef  27049  subumgredg2  27075  umgrreslem  27095  cusgrexilem2  27232  cusgrexg  27234  fusgrn0degnn0  27289  umgr2v2e  27315  vdiscusgr  27321  rusgr1vtxlem  27377  rgrusgrprc  27379  wlkon2n0  27456  upgrwlkdvdelem  27525  spthonepeq  27541  usgr2wlkneq  27545  iswwlksn  27624  wwlksnon  27637  wwlksn0  27649  wlkiswwlksupgr2  27663  wlknwwlksnbij  27674  wwlksnextbi  27680  wwlksnextfun  27684  wwlksnextinj  27685  wwlksnextbij  27688  2pthon3v  27729  umgr2wlk  27735  rusgrnumwwlkb0  27757  isclwwlkn  27812  clwwlkn1loopb  27828  hashecclwwlkn1  27862  s2elclwwlknon2  27889  uhgr3cyclex  27967  frgrwopreglem4a  28095  frgrwopreglem3  28099  frgrwopreglem5lem  28105  frgrwopreglem5  28106  frgrregorufr0  28109  friendshipgt3  28183  nvz  28452  nmlno0i  28577  norm1exi  29033  pjoc1  29217  pjoc2  29222  pj11  29497  elnlfn  29711  nmlnop0  29781  adjbd1o  29868  strlem1  30033  stcltr1i  30057  2ndimaxp  30409  fnpreimac  30434  isarchi  30861  qtophaus  31189  locfinreflem  31193  rhmpreimacn  31238  isrrext  31351  indf1ofs  31395  eulerpartlemsv3  31729  eulerpartlemgvv  31744  ballotlemelo  31855  ballotlemfmpn  31862  ballotlemiex  31869  ballotlemi1  31870  ballotlemii  31871  ballotlemfrcn0  31897  ballotlemirc  31899  bnj229  32266  bnj517  32267  bnj590  32292  bnj1097  32363  bnj1118  32366  bnj1128  32372  bnj1145  32375  f1resfz0f1d  32471  loop1cycl  32497  umgr2cycl  32501  subfacp1lem3  32542  cvmlift3lem5  32683  satffunlem1lem1  32762  satffunlem2lem1  32764  satffunlem2lem2  32766  mthmi  32937  trpred0  33188  nosupfv  33319  noeta  33335  nocvxmin  33361  scutbday  33380  scutun12  33384  scutbdaylt  33389  rankeq1o  33745  finxpreclem6  34813  poimirlem13  35070  poimirlem14  35071  poimirlem17  35074  poimirlem18  35075  poimirlem21  35078  poimirlem27  35084  poimirlem28  35085  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  lfl1  36366  lshpkrex  36414  cdleme50rnlem  37840  dochkr1  38774  dochkr1OLDN  38775  lcfrlem28  38866  mapd1o  38944  hdmap1vallem  39093  diophrw  39700  eldioph3  39707  diophin  39713  eq0rabdioph  39717  eldioph4b  39752  fphpdo  39758  fnwe2lem2  39995  fnwe2lem3  39996  islssfgi  40016  hbt  40074  dgraaval  40088  dgraalem  40089  dgraaub  40092  mpaaeu  40094  mpaaval  40095  mpaalem  40096  rngunsnply  40117  idomsubgmo  40142  proot1mul  40143  fvelrnbf  41647  wessf1ornlem  41811  sumnnodd  42272  fourierdlem2  42751  fourierdlem3  42752  uniimafveqt  43898  elsetpreimafvrab  43911  prpair  44018  prproropf1olem1  44020  pairreueq  44027  paireqne  44028  prprspr2  44035  reuprpr  44040  requad2  44141  uspgrsprfo  44376  ply1mulgsumlem2  44795  lindslinindsimp1  44866  snlindsntor  44880  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  nn0sumshdiglem1  45035  nn0sumshdig  45037