Theorem fveqeq2 6894

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6496  df-fv 6548

This theorem is referenced by:  fvelimad  6952  dff13f  7257  f1veqaeq  7258  f1elima  7265  fpropnf1  7269  nf1const  7306  oteqimp  8008  fimaproj  8134  suppfnss  8188  suppssfv  8201  tz7.48lem  8431  seqomlem1  8440  seqomlem2  8441  fofinf1o  9292  fipreima  9318  cantnfp1lem3  9652  brttrcl2  9686  ssttrcl  9687  ttrcltr  9688  tcrank  9859  updjudhcoinlf  9921  updjudhcoinrg  9922  pm54.43lem  9989  ackbij1lem18  10222  ackbij1  10223  axcc2  10424  iunfo  10526  grur1  10808  injresinjlem  13822  injresinj  13823  suppssfz  14033  seqid2  14087  hashrabsn01  14412  hashrabsn1  14413  hashimarni  14481  hashbclem  14492  hashbc  14493  hash2exprb  14511  elss2prb  14528  hash2sspr  14529  hash3tpde  14533  fi1uzind  14547  brfi1indALT  14550  wrdmap  14586  wrdl1s1  14655  wrdind  14762  wrd2ind  14763  reuccatpfxs1lem  14786  reuccatpfxs1  14787  cshf1  14850  cshw1  14862  wwlktovf  14996  wwlktovf1  14997  wwlktovfo  14998  wrd2f1tovbij  15000  wrdl3s3  15002  abs1m  15390  sumrblem  15765  fsumcvg  15766  summolem2a  15769  incexc2  15895  ntrivcvgfvn0  15956  prodrblem  15986  fprodcvg  15987  prodmolem2a  15991  smupvallem  16544  smu01lem  16546  algfx  16641  iserodd  16898  prmreclem2  16980  prmreclem3  16981  vdwlem2  17045  vdwlem6  17049  vdwlem8  17051  hashbcval  17065  ramub1lem1  17089  ramub1lem2  17090  imasleval  17598  eldmcoa  18125  coaval  18128  ghmf1  19319  ghmqusnsglem1  19353  ghmquskerlem1  19356  orbsta  19386  symgextf1  19494  psgnunilem2  19568  psgnunilem3  19569  psgnunilem4  19570  odeq1  19633  odngen  19650  sylow1lem2  19672  sylow1lem4  19674  sylow1lem5  19675  pgpfi  19678  efgtlen  19799  efgsfo  19812  efgredlemd  19817  efgred  19821  gsummptnn0fzfv  20060  isabvd  20898  abveq0  20904  abvdom  20916  islbs  21180  isobs  21853  cply1mul  22439  mdetunilem1  22752  mdetunilem4  22755  mdetunilem8  22759  mdetunilem9  22760  pmatcoe1fsupp  22841  m2cpminvid2lem  22894  mp2pm2mplem4  22949  2ndci  23588  2ndcsb  23589  2ndcsep  23599  txkgen  23792  nmoeq0  24876  nmoleub3  25261  ivth  25596  ivthle  25598  ivthle2  25599  ovolunlem1  25639  ovolicc2  25664  volivth  25749  mbfinf  25807  itg2splitlem  25890  rollelem  26131  rolle  26132  tdeglem4  26200  mdeglt  26205  deg1leb  26235  deg1lt  26237  fta1g  26310  ig1peu  26315  ig1pval3  26318  dgrle  26383  0dgrb  26386  dgreq0  26405  fta1lem  26451  fta1  26452  aannenlem1  26472  aannenlem2  26473  aalioulem2  26477  reeff1o  26590  eflogeq  26747  argregt0  26755  argrege0  26756  efopn  26803  asinsinb  27042  acoscosb  27043  atantanb  27069  musum  27335  dchrptlem1  27408  dchrptlem2  27409  lgsquadlem1  27524  nosupcbv  27846  nosupfv  27850  noinfcbv  27861  noinffv  27865  nocvxmin  27928  cutbday  27957  eqcuts  27958  cutsun12  27963  cutbdaylt  27971  cuteq0  27988  negleft  28231  negright  28232  oniso  28444  bdayn0sf1o  28543  dfnns2  28545  znegscl  28565  renegscl  28671  istrkgl  28707  mirreu  28921  israg  28956  lmireu  29077  lmieq  29078  gropd  29351  grstructd  29352  umgredg2  29420  umgrbi  29421  umgrnloopv  29426  umgredgprv  29427  edgumgr  29455  numedglnl  29464  umgredgnlp  29467  edgusgr  29480  usgruspgrb  29503  uhgr2edg  29528  usgredg2v  29547  ushgredgedgloop  29551  usgr1e  29565  usgrexmplef  29579  subumgredg2  29605  umgrreslem  29625  cusgrexilem2  29762  cusgrexg  29764  fusgrn0degnn0  29819  umgr2v2e  29845  vdiscusgr  29851  rusgr1vtxlem  29907  rgrusgrprc  29909  wlkon2n0  29984  upgrwlkdvdelem  30055  spthonepeq  30071  usgr2wlkneq  30075  iswwlksn  30157  wwlksnon  30170  wwlksn0  30182  wlkiswwlksupgr2  30196  wlknwwlksnbij  30207  wwlksnextbi  30213  wwlksnextfun  30217  wwlksnextinj  30218  wwlksnextbij  30221  2pthon3v  30262  umgr2wlk  30268  rusgrnumwwlkb0  30293  isclwwlkn  30348  clwwlkn1loopb  30364  hashecclwwlkn1  30398  s2elclwwlknon2  30425  uhgr3cyclex  30503  frgrwopreglem4a  30631  frgrwopreglem3  30635  frgrwopreglem5lem  30641  frgrwopreglem5  30642  frgrregorufr0  30645  friendshipgt3  30719  nvz  30991  nmlno0i  31116  norm1exi  31572  pjoc1  31756  pjoc2  31761  pj11  32036  elnlfn  32250  nmlnop0  32320  adjbd1o  32407  strlem1  32572  stcltr1i  32596  2ndimaxp  32961  fnpreimac  32985  indf1ofs  33156  isarchi  33472  ply1dg1rt  33840  extvfval  33892  esplyfval0  33924  esplymhp  33928  esplyfv1  33929  vieta  33940  minplyval  34065  qtophaus  34196  locfinreflem  34200  rhmpreimacn  34245  isrrext  34360  eulerpartlemsv3  34721  eulerpartlemgvv  34736  ballotlemelo  34848  ballotlemfmpn  34855  ballotlemiex  34862  ballotlemi1  34863  ballotlemii  34864  ballotlemfrcn0  34890  ballotlemirc  34892  bnj229  35242  bnj517  35243  bnj590  35268  bnj1097  35339  bnj1118  35342  bnj1128  35348  bnj1145  35351  kardeng  35528  vonf1oonfo  35557  f1resfz0f1d  35563  loop1cycl  35587  umgr2cycl  35591  subfacp1lem3  35632  cvmlift3lem5  35773  satffunlem1lem1  35852  satffunlem2lem1  35854  satffunlem2lem2  35856  mthmi  36027  rankeq1o  36621  weiunfr  36926  finxpreclem6  37990  poimirlem13  38232  poimirlem14  38233  poimirlem17  38236  poimirlem18  38237  poimirlem21  38240  poimirlem27  38246  poimirlem28  38247  ovoliunnfl  38261  voliunnfl  38263  volsupnfl  38264  lfl1  39794  lshpkrex  39842  cdleme50rnlem  41268  dochkr1  42202  dochkr1OLDN  42203  lcfrlem28  42294  mapd1o  42372  hdmap1vallem  42521  aks6d1c4  42841  hashnexinjle  42846  sticksstones2  42864  sticksstones3  42865  aks6d1c6lem3  42889  aks6d1c6isolem1  42891  aks6d1c6isolem2  42892  grpods  42911  unitscyglem1  42912  unitscyglem2  42913  unitscyglem3  42914  unitscyglem4  42915  unitscyglem5  42916  diophrw  43442  eldioph3  43449  diophin  43455  eq0rabdioph  43459  eldioph4b  43490  fphpdo  43496  fnwe2lem2  43730  fnwe2lem3  43731  islssfgi  43751  hbt  43809  dgraaval  43823  dgraalem  43824  dgraaub  43827  mpaaeu  43829  mpaaval  43830  mpaalem  43831  rngunsnply  43848  idomsubgmo  43872  proot1mul  43873  cantnfresb  44003  fvelrnbf  45690  wessf1ornlem  45855  sumnnodd  46298  fourierdlem2  46775  fourierdlem3  46776  fcoresf1  47755  uniimafveqt  48079  elsetpreimafvrab  48092  prpair  48199  prproropf1olem1  48201  pairreueq  48208  paireqne  48209  prprspr2  48216  reuprpr  48221  requad2  48337  cycldlenngric  48642  uhgrimisgrgriclem  48644  clnbgrgrimlem  48647  clnbgrgrim  48648  usgrgrtrirex  48664  stgrusgra  48673  uspgrlimlem1  48702  uspgrlimlem2  48703  grlimgrtri  48717  usgrexmpl1lem  48735  usgrexmpl2lem  48740  gpgusgralem  48770  gpgprismgr4cyclex  48821  uspgrsprfo  48862  ply1mulgsumlem2  49116  lindslinindsimp1  49186  snlindsntor  49200  nn0sumshdiglemA  49348  nn0sumshdiglemB  49349  nn0sumshdiglem1  49350  nn0sumshdig  49352  istermc  50201