Theorem fveqeq2 6890

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544

This theorem is used by:  fvelimad  6948  dff13f  7253  f1veqaeq  7254  f1elima  7261  fpropnf1  7265  nf1const  7302  oteqimp  8001  fimaproj  8127  suppfnss  8181  suppssfv  8194  tz7.48lem  8424  seqomlem1  8433  seqomlem2  8434  fofinf1o  9285  fipreima  9311  cantnfp1lem3  9645  brttrcl2  9679  ssttrcl  9680  ttrcltr  9681  tcrank  9852  updjudhcoinlf  9923  updjudhcoinrg  9924  pm54.43lem  9991  ackbij1lem18  10224  ackbij1  10225  axcc2  10425  iunfo  10527  grur1  10809  injresinjlem  13824  injresinj  13825  suppssfz  14035  seqid2  14089  hashrabsn01  14414  hashrabsn1  14415  hashimarni  14483  hashbclem  14494  hashbc  14495  hash2exprb  14513  elss2prb  14530  hash2sspr  14531  hash3tpde  14535  fi1uzind  14549  brfi1indALT  14552  wrdmap  14588  wrdl1s1  14657  wrdind  14764  wrd2ind  14765  reuccatpfxs1lem  14788  reuccatpfxs1  14789  cshf1  14852  cshw1  14864  wwlktovf  14998  wwlktovf1  14999  wwlktovfo  15000  wrd2f1tovbij  15002  wrdl3s3  15004  abs1m  15392  sumrblem  15767  fsumcvg  15768  summolem2a  15771  incexc2  15897  ntrivcvgfvn0  15958  prodrblem  15988  fprodcvg  15989  prodmolem2a  15993  smupvallem  16545  smu01lem  16547  algfx  16642  iserodd  16899  prmreclem2  16981  prmreclem3  16982  vdwlem2  17046  vdwlem6  17050  vdwlem8  17052  hashbcval  17066  ramub1lem1  17090  ramub1lem2  17091  imasleval  17599  eldmcoa  18126  coaval  18129  ghmf1  19320  ghmqusnsglem1  19354  ghmquskerlem1  19357  orbsta  19387  symgextf1  19495  psgnunilem2  19569  psgnunilem3  19570  psgnunilem4  19571  odeq1  19634  odngen  19651  sylow1lem2  19673  sylow1lem4  19675  sylow1lem5  19676  pgpfi  19679  efgtlen  19800  efgsfo  19813  efgredlemd  19818  efgred  19822  gsummptnn0fzfv  20061  isabvd  20924  abveq0  20930  abvdom  20942  islbs  21206  isobs  21879  cply1mul  22465  mdetunilem1  22778  mdetunilem4  22781  mdetunilem8  22785  mdetunilem9  22786  pmatcoe1fsupp  22867  m2cpminvid2lem  22920  mp2pm2mplem4  22975  2ndci  23614  2ndcsb  23615  2ndcsep  23625  txkgen  23818  nmoeq0  24902  nmoleub3  25287  ivth  25622  ivthle  25624  ivthle2  25625  ovolunlem1  25665  ovolicc2  25690  volivth  25775  mbfinf  25833  itg2splitlem  25916  rollelem  26157  rolle  26158  tdeglem4  26226  mdeglt  26231  deg1leb  26261  deg1lt  26263  fta1g  26336  ig1peu  26341  ig1pval3  26344  dgrle  26409  0dgrb  26412  dgreq0  26431  fta1lem  26477  fta1  26478  aannenlem1  26500  aannenlem2  26501  aalioulem2  26505  reeff1o  26619  eflogeq  26776  argregt0  26784  argrege0  26785  efopn  26832  asinsinb  27071  acoscosb  27072  atantanb  27098  musum  27364  dchrptlem1  27437  dchrptlem2  27438  lgsquadlem1  27553  nosupcbv  27875  nosupfv  27879  noinfcbv  27890  noinffv  27894  nocvxmin  27957  cutbday  27986  eqcuts  27987  cutsun12  27992  cutbdaylt  28000  cuteq0  28017  negleft  28260  negright  28261  oniso  28473  bdayn0sf1o  28572  dfnns2  28574  znegscl  28594  renegscl  28700  istrkgl  28736  mirreu  28950  israg  28986  lmireu  29108  lmieq  29109  gropd  29390  grstructd  29391  umgredg2  29459  umgrbi  29460  umgrnloopv  29465  umgredgprv  29466  edgumgr  29494  numedglnl  29503  umgredgnlp  29506  edgusgr  29519  usgruspgrb  29542  uhgr2edg  29567  usgredg2v  29586  ushgredgedgloop  29590  usgr1e  29604  usgrexmplef  29618  subumgredg2  29644  umgrreslem  29664  cusgrexilem2  29801  cusgrexg  29803  fusgrn0degnn0  29858  umgr2v2e  29884  vdiscusgr  29890  rusgr1vtxlem  29946  rgrusgrprc  29948  wlkon2n0  30023  upgrwlkdvdelem  30094  spthonepeq  30110  usgr2wlkneq  30114  iswwlksn  30196  wwlksnon  30209  wwlksn0  30221  wlkiswwlksupgr2  30235  wlknwwlksnbij  30246  wwlksnextbi  30252  wwlksnextfun  30256  wwlksnextinj  30257  wwlksnextbij  30260  2pthon3v  30301  umgr2wlk  30307  rusgrnumwwlkb0  30332  isclwwlkn  30387  clwwlkn1loopb  30403  hashecclwwlkn1  30437  s2elclwwlknon2  30464  uhgr3cyclex  30542  frgrwopreglem4a  30670  frgrwopreglem3  30674  frgrwopreglem5lem  30680  frgrwopreglem5  30681  frgrregorufr0  30684  friendshipgt3  30758  nvz  31030  nmlno0i  31155  norm1exi  31611  pjoc1  31795  pjoc2  31800  pj11  32075  elnlfn  32289  nmlnop0  32359  adjbd1o  32446  strlem1  32611  stcltr1i  32635  2ndimaxp  33000  fnpreimac  33024  indf1ofs  33195  isarchi  33511  ply1dg1rt  33879  extvfval  33931  esplyfval0  33963  esplymhp  33967  esplyfv1  33968  vieta  33979  minplyval  34104  qtophaus  34235  locfinreflem  34239  rhmpreimacn  34284  isrrext  34399  eulerpartlemsv3  34760  eulerpartlemgvv  34775  ballotlemelo  34887  ballotlemfmpn  34894  ballotlemiex  34901  ballotlemi1  34902  ballotlemii  34903  ballotlemfrcn0  34929  ballotlemirc  34931  bnj229  35281  bnj517  35282  bnj590  35307  bnj1097  35378  bnj1118  35381  bnj1128  35387  bnj1145  35390  elscott2  35522  elscottrank  35523  kardeng  35578  vonf1oonfo  35607  f1resfz0f1d  35613  loop1cycl  35637  umgr2cycl  35641  subfacp1lem3  35682  cvmlift3lem5  35823  satffunlem1lem1  35902  satffunlem2lem1  35904  satffunlem2lem2  35906  mthmi  36077  rankeq1o  36671  weiunfr  37006  finxpreclem6  38070  poimirlem13  38312  poimirlem14  38313  poimirlem17  38316  poimirlem18  38317  poimirlem21  38320  poimirlem27  38326  poimirlem28  38327  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  lfl1  39872  lshpkrex  39920  cdleme50rnlem  41346  dochkr1  42280  dochkr1OLDN  42281  lcfrlem28  42372  mapd1o  42450  hdmap1vallem  42599  aks6d1c4  42919  hashnexinjle  42924  sticksstones2  42942  sticksstones3  42943  aks6d1c6lem3  42967  aks6d1c6isolem1  42969  aks6d1c6isolem2  42970  grpods  42989  unitscyglem1  42990  unitscyglem2  42991  unitscyglem3  42992  unitscyglem4  42993  unitscyglem5  42994  diophrw  43518  eldioph3  43525  diophin  43531  eq0rabdioph  43535  eldioph4b  43566  fphpdo  43572  fnwe2lem2  43806  fnwe2lem3  43807  islssfgi  43827  hbt  43885  dgraaval  43899  dgraalem  43900  dgraaub  43903  mpaaeu  43905  mpaaval  43906  mpaalem  43907  rngunsnply  43924  idomsubgmo  43948  proot1mul  43949  cantnfresb  44079  fvelrnbf  45766  wessf1ornlem  45931  sumnnodd  46374  fourierdlem2  46851  fourierdlem3  46852  fcoresf1  47834  uniimafveqt  48158  elsetpreimafvrab  48171  prpair  48278  prproropf1olem1  48280  pairreueq  48287  paireqne  48288  prprspr2  48295  reuprpr  48300  requad2  48416  cycldlenngric  48721  uhgrimisgrgriclem  48723  clnbgrgrimlem  48726  clnbgrgrim  48727  usgrgrtrirex  48743  stgrusgra  48752  uspgrlimlem1  48781  uspgrlimlem2  48782  grlimgrtri  48796  usgrexmpl1lem  48814  usgrexmpl2lem  48819  gpgusgralem  48849  gpgprismgr4cyclex  48900  uspgrsprfo  48941  ply1mulgsumlem2  49195  lindslinindsimp1  49265  snlindsntor  49279  nn0sumshdiglemA  49427  nn0sumshdiglemB  49428  nn0sumshdiglem1  49429  nn0sumshdig  49431  istermc  50280