Theorem fveqeq2 6837

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-iota 6442  df-fv 6494

This theorem is referenced by:  fvelimad  6895  dff13f  7200  f1veqaeq  7201  f1elima  7208  fpropnf1  7212  nf1const  7249  oteqimp  7951  fimaproj  8076  suppfnss  8130  suppssfv  8143  tz7.48lem  8371  seqomlem1  8380  seqomlem2  8381  fofinf1o  9233  fipreima  9259  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  13737  injresinj  13738  suppssfz  13948  seqid2  14002  hashrabsn01  14327  hashrabsn1  14328  hashimarni  14395  hashbclem  14406  hashbc  14407  hash2exprb  14425  elss2prb  14442  hash2sspr  14443  hash3tpde  14447  fi1uzind  14461  brfi1indALT  14464  wrdmap  14500  wrdl1s1  14569  wrdind  14676  wrd2ind  14677  reuccatpfxs1lem  14700  reuccatpfxs1  14701  cshf1  14764  cshw1  14776  wwlktovf  14910  wwlktovf1  14911  wwlktovfo  14912  wrd2f1tovbij  14914  wrdl3s3  14916  abs1m  15290  sumrblem  15665  fsumcvg  15666  summolem2a  15669  incexc2  15795  ntrivcvgfvn0  15856  prodrblem  15886  fprodcvg  15887  prodmolem2a  15891  smupvallem  16444  smu01lem  16446  algfx  16541  iserodd  16798  prmreclem2  16880  prmreclem3  16881  vdwlem2  16945  vdwlem6  16949  vdwlem8  16951  hashbcval  16965  ramub1lem1  16989  ramub1lem2  16990  imasleval  17497  eldmcoa  18024  coaval  18027  ghmf1  19213  ghmqusnsglem1  19247  ghmquskerlem1  19250  orbsta  19280  symgextf1  19388  psgnunilem2  19462  psgnunilem3  19463  psgnunilem4  19464  odeq1  19527  odngen  19544  sylow1lem2  19566  sylow1lem4  19568  sylow1lem5  19569  pgpfi  19572  efgtlen  19693  efgsfo  19706  efgredlemd  19711  efgred  19715  gsummptnn0fzfv  19954  isabvd  20785  abveq0  20791  abvdom  20803  islbs  21067  isobs  21696  cply1mul  22283  mdetunilem1  22596  mdetunilem4  22599  mdetunilem8  22603  mdetunilem9  22604  pmatcoe1fsupp  22685  m2cpminvid2lem  22738  mp2pm2mplem4  22793  2ndci  23432  2ndcsb  23433  2ndcsep  23443  txkgen  23636  nmoeq0  24720  nmoleub3  25105  ivth  25440  ivthle  25442  ivthle2  25443  ovolunlem1  25483  ovolicc2  25508  volivth  25593  mbfinf  25651  itg2splitlem  25734  rollelem  25975  rolle  25976  tdeglem4  26044  mdeglt  26049  deg1leb  26079  deg1lt  26081  fta1g  26154  ig1peu  26159  ig1pval3  26162  dgrle  26227  0dgrb  26230  dgreq0  26249  fta1lem  26292  fta1  26293  aannenlem1  26313  aannenlem2  26314  aalioulem2  26318  reeff1o  26431  eflogeq  26585  argregt0  26593  argrege0  26594  efopn  26641  asinsinb  26880  acoscosb  26881  atantanb  26907  musum  27173  dchrptlem1  27246  dchrptlem2  27247  lgsquadlem1  27362  nosupcbv  27685  nosupfv  27689  noinfcbv  27700  noinffv  27704  nocvxmin  27766  cutbday  27795  eqcuts  27796  cutsun12  27801  cutbdaylt  27809  cuteq0  27826  negleft  28069  negright  28070  oniso  28282  bdayn0sf1o  28381  dfnns2  28383  znegscl  28403  renegscl  28509  istrkgl  28545  mirreu  28751  israg  28784  lmireu  28877  lmieq  28878  gropd  29119  grstructd  29120  umgredg2  29188  umgrbi  29189  umgrnloopv  29194  umgredgprv  29195  edgumgr  29223  numedglnl  29232  umgredgnlp  29235  edgusgr  29248  usgruspgrb  29271  uhgr2edg  29296  usgredg2v  29315  ushgredgedgloop  29319  usgr1e  29333  usgrexmplef  29347  subumgredg2  29373  umgrreslem  29393  cusgrexilem2  29530  cusgrexg  29532  fusgrn0degnn0  29587  umgr2v2e  29613  vdiscusgr  29619  rusgr1vtxlem  29675  rgrusgrprc  29677  wlkon2n0  29752  upgrwlkdvdelem  29823  spthonepeq  29839  usgr2wlkneq  29843  iswwlksn  29925  wwlksnon  29938  wwlksn0  29950  wlkiswwlksupgr2  29964  wlknwwlksnbij  29975  wwlksnextbi  29981  wwlksnextfun  29985  wwlksnextinj  29986  wwlksnextbij  29989  2pthon3v  30030  umgr2wlk  30036  rusgrnumwwlkb0  30061  isclwwlkn  30116  clwwlkn1loopb  30132  hashecclwwlkn1  30166  s2elclwwlknon2  30193  uhgr3cyclex  30271  frgrwopreglem4a  30399  frgrwopreglem3  30403  frgrwopreglem5lem  30409  frgrwopreglem5  30410  frgrregorufr0  30413  friendshipgt3  30487  nvz  30759  nmlno0i  30884  norm1exi  31340  pjoc1  31524  pjoc2  31529  pj11  31804  elnlfn  32018  nmlnop0  32088  adjbd1o  32175  strlem1  32340  stcltr1i  32364  2ndimaxp  32739  fnpreimac  32763  indf1ofs  32946  isarchi  33264  ply1dg1rt  33672  extvfval  33725  esplyfval0  33757  esplymhp  33761  esplyfv1  33762  vieta  33773  minplyval  33898  qtophaus  34029  locfinreflem  34033  rhmpreimacn  34078  isrrext  34193  eulerpartlemsv3  34554  eulerpartlemgvv  34569  ballotlemelo  34681  ballotlemfmpn  34688  ballotlemiex  34695  ballotlemi1  34696  ballotlemii  34697  ballotlemfrcn0  34723  ballotlemirc  34725  bnj229  35075  bnj517  35076  bnj590  35101  bnj1097  35172  bnj1118  35175  bnj1128  35181  bnj1145  35184  f1resfz0f1d  35351  loop1cycl  35374  umgr2cycl  35378  subfacp1lem3  35419  cvmlift3lem5  35560  satffunlem1lem1  35639  satffunlem2lem1  35641  satffunlem2lem2  35643  mthmi  35814  rankeq1o  36408  weiunfr  36704  finxpreclem6  37767  poimirlem13  38009  poimirlem14  38010  poimirlem17  38013  poimirlem18  38014  poimirlem21  38017  poimirlem27  38023  poimirlem28  38024  ovoliunnfl  38038  voliunnfl  38040  volsupnfl  38041  lfl1  39571  lshpkrex  39619  cdleme50rnlem  41045  dochkr1  41979  dochkr1OLDN  41980  lcfrlem28  42071  mapd1o  42149  hdmap1vallem  42298  aks6d1c4  42618  hashnexinjle  42623  sticksstones2  42641  sticksstones3  42642  aks6d1c6lem3  42666  aks6d1c6isolem1  42668  aks6d1c6isolem2  42669  grpods  42688  unitscyglem1  42689  unitscyglem2  42690  unitscyglem3  42691  unitscyglem4  42692  unitscyglem5  42693  diophrw  43217  eldioph3  43224  diophin  43230  eq0rabdioph  43234  eldioph4b  43265  fphpdo  43271  fnwe2lem2  43505  fnwe2lem3  43506  islssfgi  43526  hbt  43584  dgraaval  43598  dgraalem  43599  dgraaub  43602  mpaaeu  43604  mpaaval  43605  mpaalem  43606  rngunsnply  43623  idomsubgmo  43647  proot1mul  43648  cantnfresb  43778  fvelrnbf  45475  wessf1ornlem  45640  sumnnodd  46083  fourierdlem2  46560  fourierdlem3  46561  fcoresf1  47540  uniimafveqt  47864  elsetpreimafvrab  47877  prpair  47984  prproropf1olem1  47986  pairreueq  47993  paireqne  47994  prprspr2  48001  reuprpr  48006  requad2  48122  cycldlenngric  48427  uhgrimisgrgriclem  48429  clnbgrgrimlem  48432  clnbgrgrim  48433  usgrgrtrirex  48449  stgrusgra  48458  uspgrlimlem1  48487  uspgrlimlem2  48488  grlimgrtri  48502  usgrexmpl1lem  48520  usgrexmpl2lem  48525  gpgusgralem  48555  gpgprismgr4cyclex  48606  uspgrsprfo  48647  ply1mulgsumlem2  48886  lindslinindsimp1  48956  snlindsntor  48970  nn0sumshdiglemA  49118  nn0sumshdiglemB  49119  nn0sumshdiglem1  49120  nn0sumshdig  49122  istermc  49972