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 1540  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490

This theorem is referenced by:  fvelimad  6890  dff13f  7192  f1veqaeq  7193  f1elima  7200  fpropnf1  7204  nf1const  7241  oteqimp  7943  fimaproj  8068  suppfnss  8122  suppssfv  8135  tz7.48lem  8363  seqomlem1  8372  seqomlem2  8373  fofinf1o  9222  fipreima  9248  cantnfp1lem3  9576  brttrcl2  9610  ssttrcl  9611  ttrcltr  9612  tcrank  9780  updjudhcoinlf  9828  updjudhcoinrg  9829  pm54.43lem  9896  ackbij1lem18  10130  ackbij1  10131  axcc2  10331  iunfo  10433  grur1  10714  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  14521  wrdind  14628  wrd2ind  14629  reuccatpfxs1lem  14652  reuccatpfxs1  14653  cshf1  14716  cshw1  14728  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  19125  ghmqusnsglem1  19159  ghmquskerlem1  19162  orbsta  19192  symgextf1  19300  psgnunilem2  19374  psgnunilem3  19375  psgnunilem4  19376  odeq1  19439  odngen  19456  sylow1lem2  19478  sylow1lem4  19480  sylow1lem5  19481  pgpfi  19484  efgtlen  19605  efgsfo  19618  efgredlemd  19623  efgred  19627  gsummptnn0fzfv  19866  isabvd  20697  abveq0  20703  abvdom  20715  islbs  20980  isobs  21627  cply1mul  22181  mdetunilem1  22497  mdetunilem4  22500  mdetunilem8  22504  mdetunilem9  22505  pmatcoe1fsupp  22586  m2cpminvid2lem  22639  mp2pm2mplem4  22694  2ndci  23333  2ndcsb  23334  2ndcsep  23344  txkgen  23537  nmoeq0  24622  nmoleub3  25017  ivth  25353  ivthle  25355  ivthle2  25356  ovolunlem1  25396  ovolicc2  25421  volivth  25506  mbfinf  25564  itg2splitlem  25647  rollelem  25891  rolle  25892  tdeglem4  25963  mdeglt  25968  deg1leb  25998  deg1lt  26000  fta1g  26073  ig1peu  26078  ig1pval3  26081  dgrle  26146  0dgrb  26149  dgreq0  26169  fta1lem  26213  fta1  26214  aannenlem1  26234  aannenlem2  26235  aalioulem2  26239  reeff1o  26355  eflogeq  26509  argregt0  26517  argrege0  26518  efopn  26565  asinsinb  26805  acoscosb  26806  atantanb  26832  musum  27099  dchrptlem1  27173  dchrptlem2  27174  lgsquadlem1  27289  nosupcbv  27612  nosupfv  27616  noinfcbv  27627  noinffv  27631  nocvxmin  27689  scutbday  27715  eqscut  27716  scutun12  27721  scutbdaylt  27729  cuteq0  27746  onsiso  28174  bdayn0sf1o  28264  dfnns2  28266  znegscl  28285  renegscl  28367  istrkgl  28403  mirreu  28609  israg  28642  lmireu  28735  lmieq  28736  gropd  28976  grstructd  28977  umgredg2  29045  umgrbi  29046  umgrnloopv  29051  umgredgprv  29052  edgumgr  29080  numedglnl  29089  umgredgnlp  29092  edgusgr  29105  usgruspgrb  29128  uhgr2edg  29153  usgredg2v  29172  ushgredgedgloop  29176  usgr1e  29190  usgrexmplef  29204  subumgredg2  29230  umgrreslem  29250  cusgrexilem2  29387  cusgrexg  29389  fusgrn0degnn0  29445  umgr2v2e  29471  vdiscusgr  29477  rusgr1vtxlem  29533  rgrusgrprc  29535  wlkon2n0  29610  upgrwlkdvdelem  29681  spthonepeq  29697  usgr2wlkneq  29701  iswwlksn  29783  wwlksnon  29796  wwlksn0  29808  wlkiswwlksupgr2  29822  wlknwwlksnbij  29833  wwlksnextbi  29839  wwlksnextfun  29843  wwlksnextinj  29844  wwlksnextbij  29847  2pthon3v  29888  umgr2wlk  29894  rusgrnumwwlkb0  29916  isclwwlkn  29971  clwwlkn1loopb  29987  hashecclwwlkn1  30021  s2elclwwlknon2  30048  uhgr3cyclex  30126  frgrwopreglem4a  30254  frgrwopreglem3  30258  frgrwopreglem5lem  30264  frgrwopreglem5  30265  frgrregorufr0  30268  friendshipgt3  30342  nvz  30613  nmlno0i  30738  norm1exi  31194  pjoc1  31378  pjoc2  31383  pj11  31658  elnlfn  31872  nmlnop0  31942  adjbd1o  32029  strlem1  32194  stcltr1i  32218  2ndimaxp  32590  fnpreimac  32615  indf1ofs  32810  isarchi  33125  ply1dg1rt  33516  minplyval  33678  qtophaus  33809  locfinreflem  33813  rhmpreimacn  33858  isrrext  33973  eulerpartlemsv3  34335  eulerpartlemgvv  34350  ballotlemelo  34462  ballotlemfmpn  34469  ballotlemiex  34476  ballotlemi1  34477  ballotlemii  34478  ballotlemfrcn0  34504  ballotlemirc  34506  bnj229  34857  bnj517  34858  bnj590  34883  bnj1097  34954  bnj1118  34957  bnj1128  34963  bnj1145  34966  f1resfz0f1d  35097  loop1cycl  35120  umgr2cycl  35124  subfacp1lem3  35165  cvmlift3lem5  35306  satffunlem1lem1  35385  satffunlem2lem1  35387  satffunlem2lem2  35389  mthmi  35560  rankeq1o  36155  weiunfr  36451  finxpreclem6  37380  poimirlem13  37623  poimirlem14  37624  poimirlem17  37627  poimirlem18  37628  poimirlem21  37631  poimirlem27  37637  poimirlem28  37638  ovoliunnfl  37652  voliunnfl  37654  volsupnfl  37655  lfl1  39059  lshpkrex  39107  cdleme50rnlem  40533  dochkr1  41467  dochkr1OLDN  41468  lcfrlem28  41559  mapd1o  41637  hdmap1vallem  41786  aks6d1c4  42107  hashnexinjle  42112  sticksstones2  42130  sticksstones3  42131  aks6d1c6lem3  42155  aks6d1c6isolem1  42157  aks6d1c6isolem2  42158  grpods  42177  unitscyglem1  42178  unitscyglem2  42179  unitscyglem3  42180  unitscyglem4  42181  unitscyglem5  42182  diophrw  42742  eldioph3  42749  diophin  42755  eq0rabdioph  42759  eldioph4b  42794  fphpdo  42800  fnwe2lem2  43034  fnwe2lem3  43035  islssfgi  43055  hbt  43113  dgraaval  43127  dgraalem  43128  dgraaub  43131  mpaaeu  43133  mpaaval  43134  mpaalem  43135  rngunsnply  43152  idomsubgmo  43176  proot1mul  43177  cantnfresb  43307  fvelrnbf  45006  wessf1ornlem  45173  sumnnodd  45621  fourierdlem2  46100  fourierdlem3  46101  fcoresf1  47063  uniimafveqt  47375  elsetpreimafvrab  47388  prpair  47495  prproropf1olem1  47497  pairreueq  47504  paireqne  47505  prprspr2  47512  reuprpr  47517  requad2  47617  cycldlenngric  47922  uhgrimisgrgriclem  47924  clnbgrgrimlem  47927  clnbgrgrim  47928  usgrgrtrirex  47944  stgrusgra  47953  uspgrlimlem1  47982  uspgrlimlem2  47983  grlimgrtri  47997  usgrexmpl1lem  48015  usgrexmpl2lem  48020  gpgusgralem  48050  gpgprismgr4cyclex  48101  uspgrsprfo  48142  ply1mulgsumlem2  48382  lindslinindsimp1  48452  snlindsntor  48466  nn0sumshdiglemA  48614  nn0sumshdiglemB  48615  nn0sumshdiglem1  48616  nn0sumshdig  48618  istermc  49469