Theorem fveqeq2 6844

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ‘cfv 6493

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501

This theorem is referenced by:  fvelimad  6902  dff13f  7203  f1veqaeq  7204  f1elima  7211  fpropnf1  7215  nf1const  7252  oteqimp  7954  fimaproj  8079  suppfnss  8133  suppssfv  8146  tz7.48lem  8374  seqomlem1  8383  seqomlem2  8384  fofinf1o  9236  fipreima  9262  cantnfp1lem3  9593  brttrcl2  9627  ssttrcl  9628  ttrcltr  9629  tcrank  9800  updjudhcoinlf  9848  updjudhcoinrg  9849  pm54.43lem  9916  ackbij1lem18  10150  ackbij1  10151  axcc2  10351  iunfo  10453  grur1  10735  injresinjlem  13710  injresinj  13711  suppssfz  13921  seqid2  13975  hashrabsn01  14300  hashrabsn1  14301  hashimarni  14368  hashbclem  14379  hashbc  14380  hash2exprb  14398  elss2prb  14415  hash2sspr  14416  hash3tpde  14420  fi1uzind  14434  brfi1indALT  14437  wrdmap  14473  wrdl1s1  14542  wrdind  14649  wrd2ind  14650  reuccatpfxs1lem  14673  reuccatpfxs1  14674  cshf1  14737  cshw1  14749  wwlktovf  14883  wwlktovf1  14884  wwlktovfo  14885  wrd2f1tovbij  14887  wrdl3s3  14889  abs1m  15263  sumrblem  15638  fsumcvg  15639  summolem2a  15642  incexc2  15765  ntrivcvgfvn0  15826  prodrblem  15856  fprodcvg  15857  prodmolem2a  15861  smupvallem  16414  smu01lem  16416  algfx  16511  iserodd  16767  prmreclem2  16849  prmreclem3  16850  vdwlem2  16914  vdwlem6  16918  vdwlem8  16920  hashbcval  16934  ramub1lem1  16958  ramub1lem2  16959  imasleval  17466  eldmcoa  17993  coaval  17996  ghmf1  19179  ghmqusnsglem1  19213  ghmquskerlem1  19216  orbsta  19246  symgextf1  19354  psgnunilem2  19428  psgnunilem3  19429  psgnunilem4  19430  odeq1  19493  odngen  19510  sylow1lem2  19532  sylow1lem4  19534  sylow1lem5  19535  pgpfi  19538  efgtlen  19659  efgsfo  19672  efgredlemd  19677  efgred  19681  gsummptnn0fzfv  19920  isabvd  20749  abveq0  20755  abvdom  20767  islbs  21032  isobs  21679  cply1mul  22244  mdetunilem1  22560  mdetunilem4  22563  mdetunilem8  22567  mdetunilem9  22568  pmatcoe1fsupp  22649  m2cpminvid2lem  22702  mp2pm2mplem4  22757  2ndci  23396  2ndcsb  23397  2ndcsep  23407  txkgen  23600  nmoeq0  24684  nmoleub3  25079  ivth  25415  ivthle  25417  ivthle2  25418  ovolunlem1  25458  ovolicc2  25483  volivth  25568  mbfinf  25626  itg2splitlem  25709  rollelem  25953  rolle  25954  tdeglem4  26025  mdeglt  26030  deg1leb  26060  deg1lt  26062  fta1g  26135  ig1peu  26140  ig1pval3  26143  dgrle  26208  0dgrb  26211  dgreq0  26231  fta1lem  26275  fta1  26276  aannenlem1  26296  aannenlem2  26297  aalioulem2  26301  reeff1o  26417  eflogeq  26571  argregt0  26579  argrege0  26580  efopn  26627  asinsinb  26867  acoscosb  26868  atantanb  26894  musum  27161  dchrptlem1  27235  dchrptlem2  27236  lgsquadlem1  27351  nosupcbv  27674  nosupfv  27678  noinfcbv  27689  noinffv  27693  nocvxmin  27755  cutbday  27784  eqcuts  27785  cutsun12  27790  cutbdaylt  27798  cuteq0  27815  negleft  28058  negright  28059  oniso  28271  bdayn0sf1o  28370  dfnns2  28372  znegscl  28392  renegscl  28498  istrkgl  28534  mirreu  28740  israg  28773  lmireu  28866  lmieq  28867  gropd  29108  grstructd  29109  umgredg2  29177  umgrbi  29178  umgrnloopv  29183  umgredgprv  29184  edgumgr  29212  numedglnl  29221  umgredgnlp  29224  edgusgr  29237  usgruspgrb  29260  uhgr2edg  29285  usgredg2v  29304  ushgredgedgloop  29308  usgr1e  29322  usgrexmplef  29336  subumgredg2  29362  umgrreslem  29382  cusgrexilem2  29519  cusgrexg  29521  fusgrn0degnn0  29577  umgr2v2e  29603  vdiscusgr  29609  rusgr1vtxlem  29665  rgrusgrprc  29667  wlkon2n0  29742  upgrwlkdvdelem  29813  spthonepeq  29829  usgr2wlkneq  29833  iswwlksn  29915  wwlksnon  29928  wwlksn0  29940  wlkiswwlksupgr2  29954  wlknwwlksnbij  29965  wwlksnextbi  29971  wwlksnextfun  29975  wwlksnextinj  29976  wwlksnextbij  29979  2pthon3v  30020  umgr2wlk  30026  rusgrnumwwlkb0  30051  isclwwlkn  30106  clwwlkn1loopb  30122  hashecclwwlkn1  30156  s2elclwwlknon2  30183  uhgr3cyclex  30261  frgrwopreglem4a  30389  frgrwopreglem3  30393  frgrwopreglem5lem  30399  frgrwopreglem5  30400  frgrregorufr0  30403  friendshipgt3  30477  nvz  30748  nmlno0i  30873  norm1exi  31329  pjoc1  31513  pjoc2  31518  pj11  31793  elnlfn  32007  nmlnop0  32077  adjbd1o  32164  strlem1  32329  stcltr1i  32353  2ndimaxp  32727  fnpreimac  32751  indf1ofs  32950  isarchi  33266  ply1dg1rt  33663  extvfval  33699  esplyfval0  33724  esplymhp  33728  esplyfv1  33729  vieta  33738  minplyval  33864  qtophaus  33995  locfinreflem  33999  rhmpreimacn  34044  isrrext  34159  eulerpartlemsv3  34520  eulerpartlemgvv  34535  ballotlemelo  34647  ballotlemfmpn  34654  ballotlemiex  34661  ballotlemi1  34662  ballotlemii  34663  ballotlemfrcn0  34689  ballotlemirc  34691  bnj229  35042  bnj517  35043  bnj590  35068  bnj1097  35139  bnj1118  35142  bnj1128  35148  bnj1145  35151  f1resfz0f1d  35310  loop1cycl  35333  umgr2cycl  35337  subfacp1lem3  35378  cvmlift3lem5  35519  satffunlem1lem1  35598  satffunlem2lem1  35600  satffunlem2lem2  35602  mthmi  35773  rankeq1o  36367  weiunfr  36663  finxpreclem6  37603  poimirlem13  37836  poimirlem14  37837  poimirlem17  37840  poimirlem18  37841  poimirlem21  37844  poimirlem27  37850  poimirlem28  37851  ovoliunnfl  37865  voliunnfl  37867  volsupnfl  37868  lfl1  39398  lshpkrex  39446  cdleme50rnlem  40872  dochkr1  41806  dochkr1OLDN  41807  lcfrlem28  41898  mapd1o  41976  hdmap1vallem  42125  aks6d1c4  42446  hashnexinjle  42451  sticksstones2  42469  sticksstones3  42470  aks6d1c6lem3  42494  aks6d1c6isolem1  42496  aks6d1c6isolem2  42497  grpods  42516  unitscyglem1  42517  unitscyglem2  42518  unitscyglem3  42519  unitscyglem4  42520  unitscyglem5  42521  diophrw  43068  eldioph3  43075  diophin  43081  eq0rabdioph  43085  eldioph4b  43120  fphpdo  43126  fnwe2lem2  43360  fnwe2lem3  43361  islssfgi  43381  hbt  43439  dgraaval  43453  dgraalem  43454  dgraaub  43457  mpaaeu  43459  mpaaval  43460  mpaalem  43461  rngunsnply  43478  idomsubgmo  43502  proot1mul  43503  cantnfresb  43633  fvelrnbf  45330  wessf1ornlem  45496  sumnnodd  45943  fourierdlem2  46420  fourierdlem3  46421  fcoresf1  47382  uniimafveqt  47694  elsetpreimafvrab  47707  prpair  47814  prproropf1olem1  47816  pairreueq  47823  paireqne  47824  prprspr2  47831  reuprpr  47836  requad2  47936  cycldlenngric  48241  uhgrimisgrgriclem  48243  clnbgrgrimlem  48246  clnbgrgrim  48247  usgrgrtrirex  48263  stgrusgra  48272  uspgrlimlem1  48301  uspgrlimlem2  48302  grlimgrtri  48316  usgrexmpl1lem  48334  usgrexmpl2lem  48339  gpgusgralem  48369  gpgprismgr4cyclex  48420  uspgrsprfo  48461  ply1mulgsumlem2  48700  lindslinindsimp1  48770  snlindsntor  48784  nn0sumshdiglemA  48932  nn0sumshdiglemB  48933  nn0sumshdiglem1  48934  nn0sumshdig  48936  istermc  49786