Theorem fveqeq2 6831

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489

This theorem is referenced by:  fvelimad  6889  dff13f  7189  f1veqaeq  7190  f1elima  7197  fpropnf1  7201  nf1const  7238  oteqimp  7940  fimaproj  8065  suppfnss  8119  suppssfv  8132  tz7.48lem  8360  seqomlem1  8369  seqomlem2  8370  fofinf1o  9216  fipreima  9242  cantnfp1lem3  9570  brttrcl2  9604  ssttrcl  9605  ttrcltr  9606  tcrank  9777  updjudhcoinlf  9825  updjudhcoinrg  9826  pm54.43lem  9893  ackbij1lem18  10127  ackbij1  10128  axcc2  10328  iunfo  10430  grur1  10711  injresinjlem  13690  injresinj  13691  suppssfz  13901  seqid2  13955  hashrabsn01  14280  hashrabsn1  14281  hashimarni  14348  hashbclem  14359  hashbc  14360  hash2exprb  14378  elss2prb  14395  hash2sspr  14396  hash3tpde  14400  fi1uzind  14414  brfi1indALT  14417  wrdmap  14453  wrdl1s1  14522  wrdind  14629  wrd2ind  14630  reuccatpfxs1lem  14653  reuccatpfxs1  14654  cshf1  14717  cshw1  14729  wwlktovf  14863  wwlktovf1  14864  wwlktovfo  14865  wrd2f1tovbij  14867  wrdl3s3  14869  abs1m  15243  sumrblem  15618  fsumcvg  15619  summolem2a  15622  incexc2  15745  ntrivcvgfvn0  15806  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  smupvallem  16394  smu01lem  16396  algfx  16491  iserodd  16747  prmreclem2  16829  prmreclem3  16830  vdwlem2  16894  vdwlem6  16898  vdwlem8  16900  hashbcval  16914  ramub1lem1  16938  ramub1lem2  16939  imasleval  17445  eldmcoa  17972  coaval  17975  ghmf1  19158  ghmqusnsglem1  19192  ghmquskerlem1  19195  orbsta  19225  symgextf1  19333  psgnunilem2  19407  psgnunilem3  19408  psgnunilem4  19409  odeq1  19472  odngen  19489  sylow1lem2  19511  sylow1lem4  19513  sylow1lem5  19514  pgpfi  19517  efgtlen  19638  efgsfo  19651  efgredlemd  19656  efgred  19660  gsummptnn0fzfv  19899  isabvd  20727  abveq0  20733  abvdom  20745  islbs  21010  isobs  21657  cply1mul  22211  mdetunilem1  22527  mdetunilem4  22530  mdetunilem8  22534  mdetunilem9  22535  pmatcoe1fsupp  22616  m2cpminvid2lem  22669  mp2pm2mplem4  22724  2ndci  23363  2ndcsb  23364  2ndcsep  23374  txkgen  23567  nmoeq0  24651  nmoleub3  25046  ivth  25382  ivthle  25384  ivthle2  25385  ovolunlem1  25425  ovolicc2  25450  volivth  25535  mbfinf  25593  itg2splitlem  25676  rollelem  25920  rolle  25921  tdeglem4  25992  mdeglt  25997  deg1leb  26027  deg1lt  26029  fta1g  26102  ig1peu  26107  ig1pval3  26110  dgrle  26175  0dgrb  26178  dgreq0  26198  fta1lem  26242  fta1  26243  aannenlem1  26263  aannenlem2  26264  aalioulem2  26268  reeff1o  26384  eflogeq  26538  argregt0  26546  argrege0  26547  efopn  26594  asinsinb  26834  acoscosb  26835  atantanb  26861  musum  27128  dchrptlem1  27202  dchrptlem2  27203  lgsquadlem1  27318  nosupcbv  27641  nosupfv  27645  noinfcbv  27656  noinffv  27660  nocvxmin  27718  scutbday  27745  eqscut  27746  scutun12  27751  scutbdaylt  27759  cuteq0  27776  onsiso  28205  bdayn0sf1o  28295  dfnns2  28297  znegscl  28316  renegscl  28400  istrkgl  28436  mirreu  28642  israg  28675  lmireu  28768  lmieq  28769  gropd  29009  grstructd  29010  umgredg2  29078  umgrbi  29079  umgrnloopv  29084  umgredgprv  29085  edgumgr  29113  numedglnl  29122  umgredgnlp  29125  edgusgr  29138  usgruspgrb  29161  uhgr2edg  29186  usgredg2v  29205  ushgredgedgloop  29209  usgr1e  29223  usgrexmplef  29237  subumgredg2  29263  umgrreslem  29283  cusgrexilem2  29420  cusgrexg  29422  fusgrn0degnn0  29478  umgr2v2e  29504  vdiscusgr  29510  rusgr1vtxlem  29566  rgrusgrprc  29568  wlkon2n0  29643  upgrwlkdvdelem  29714  spthonepeq  29730  usgr2wlkneq  29734  iswwlksn  29816  wwlksnon  29829  wwlksn0  29841  wlkiswwlksupgr2  29855  wlknwwlksnbij  29866  wwlksnextbi  29872  wwlksnextfun  29876  wwlksnextinj  29877  wwlksnextbij  29880  2pthon3v  29921  umgr2wlk  29927  rusgrnumwwlkb0  29952  isclwwlkn  30007  clwwlkn1loopb  30023  hashecclwwlkn1  30057  s2elclwwlknon2  30084  uhgr3cyclex  30162  frgrwopreglem4a  30290  frgrwopreglem3  30294  frgrwopreglem5lem  30300  frgrwopreglem5  30301  frgrregorufr0  30304  friendshipgt3  30378  nvz  30649  nmlno0i  30774  norm1exi  31230  pjoc1  31414  pjoc2  31419  pj11  31694  elnlfn  31908  nmlnop0  31978  adjbd1o  32065  strlem1  32230  stcltr1i  32254  2ndimaxp  32628  fnpreimac  32653  indf1ofs  32847  isarchi  33151  ply1dg1rt  33543  esplymhp  33589  esplyfv1  33590  minplyval  33718  qtophaus  33849  locfinreflem  33853  rhmpreimacn  33898  isrrext  34013  eulerpartlemsv3  34374  eulerpartlemgvv  34389  ballotlemelo  34501  ballotlemfmpn  34508  ballotlemiex  34515  ballotlemi1  34516  ballotlemii  34517  ballotlemfrcn0  34543  ballotlemirc  34545  bnj229  34896  bnj517  34897  bnj590  34922  bnj1097  34993  bnj1118  34996  bnj1128  35002  bnj1145  35005  f1resfz0f1d  35158  loop1cycl  35181  umgr2cycl  35185  subfacp1lem3  35226  cvmlift3lem5  35367  satffunlem1lem1  35446  satffunlem2lem1  35448  satffunlem2lem2  35450  mthmi  35621  rankeq1o  36215  weiunfr  36511  finxpreclem6  37440  poimirlem13  37672  poimirlem14  37673  poimirlem17  37676  poimirlem18  37677  poimirlem21  37680  poimirlem27  37686  poimirlem28  37687  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  lfl1  39168  lshpkrex  39216  cdleme50rnlem  40642  dochkr1  41576  dochkr1OLDN  41577  lcfrlem28  41668  mapd1o  41746  hdmap1vallem  41895  aks6d1c4  42216  hashnexinjle  42221  sticksstones2  42239  sticksstones3  42240  aks6d1c6lem3  42264  aks6d1c6isolem1  42266  aks6d1c6isolem2  42267  grpods  42286  unitscyglem1  42287  unitscyglem2  42288  unitscyglem3  42289  unitscyglem4  42290  unitscyglem5  42291  diophrw  42851  eldioph3  42858  diophin  42864  eq0rabdioph  42868  eldioph4b  42903  fphpdo  42909  fnwe2lem2  43143  fnwe2lem3  43144  islssfgi  43164  hbt  43222  dgraaval  43236  dgraalem  43237  dgraaub  43240  mpaaeu  43242  mpaaval  43243  mpaalem  43244  rngunsnply  43261  idomsubgmo  43285  proot1mul  43286  cantnfresb  43416  fvelrnbf  45114  wessf1ornlem  45281  sumnnodd  45729  fourierdlem2  46206  fourierdlem3  46207  fcoresf1  47168  uniimafveqt  47480  elsetpreimafvrab  47493  prpair  47600  prproropf1olem1  47602  pairreueq  47609  paireqne  47610  prprspr2  47617  reuprpr  47622  requad2  47722  cycldlenngric  48027  uhgrimisgrgriclem  48029  clnbgrgrimlem  48032  clnbgrgrim  48033  usgrgrtrirex  48049  stgrusgra  48058  uspgrlimlem1  48087  uspgrlimlem2  48088  grlimgrtri  48102  usgrexmpl1lem  48120  usgrexmpl2lem  48125  gpgusgralem  48155  gpgprismgr4cyclex  48206  uspgrsprfo  48247  ply1mulgsumlem2  48487  lindslinindsimp1  48557  snlindsntor  48571  nn0sumshdiglemA  48719  nn0sumshdiglemB  48720  nn0sumshdiglem1  48721  nn0sumshdig  48723  istermc  49574