Theorem fveqeq2 6867

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ‘cfv 6511

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519

This theorem is referenced by:  fvelimad  6928  dff13f  7230  f1veqaeq  7231  f1elima  7238  fpropnf1  7242  nf1const  7279  oteqimp  7987  fimaproj  8114  suppfnss  8168  suppssfv  8181  tz7.48lem  8409  seqomlem1  8418  seqomlem2  8419  fofinf1o  9283  fipreima  9309  cantnfp1lem3  9633  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  tcrank  9837  updjudhcoinlf  9885  updjudhcoinrg  9886  pm54.43lem  9953  ackbij1lem18  10189  ackbij1  10190  axcc2  10390  iunfo  10492  grur1  10773  injresinjlem  13748  injresinj  13749  suppssfz  13959  seqid2  14013  hashrabsn01  14338  hashrabsn1  14339  hashimarni  14406  hashbclem  14417  hashbc  14418  hash2exprb  14436  elss2prb  14453  hash2sspr  14454  hash3tpde  14458  fi1uzind  14472  brfi1indALT  14475  wrdmap  14511  wrdl1s1  14579  wrdind  14687  wrd2ind  14688  reuccatpfxs1lem  14711  reuccatpfxs1  14712  cshf1  14775  cshw1  14787  wwlktovf  14922  wwlktovf1  14923  wwlktovfo  14924  wrd2f1tovbij  14926  wrdl3s3  14928  abs1m  15302  sumrblem  15677  fsumcvg  15678  summolem2a  15681  incexc2  15804  ntrivcvgfvn0  15865  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  smupvallem  16453  smu01lem  16455  algfx  16550  iserodd  16806  prmreclem2  16888  prmreclem3  16889  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  hashbcval  16973  ramub1lem1  16997  ramub1lem2  16998  imasleval  17504  eldmcoa  18027  coaval  18030  ghmf1  19178  ghmqusnsglem1  19212  ghmquskerlem1  19215  orbsta  19245  symgextf1  19351  psgnunilem2  19425  psgnunilem3  19426  psgnunilem4  19427  odeq1  19490  odngen  19507  sylow1lem2  19529  sylow1lem4  19531  sylow1lem5  19532  pgpfi  19535  efgtlen  19656  efgsfo  19669  efgredlemd  19674  efgred  19678  gsummptnn0fzfv  19917  isabvd  20721  abveq0  20727  abvdom  20739  islbs  20983  isobs  21629  cply1mul  22183  mdetunilem1  22499  mdetunilem4  22502  mdetunilem8  22506  mdetunilem9  22507  pmatcoe1fsupp  22588  m2cpminvid2lem  22641  mp2pm2mplem4  22696  2ndci  23335  2ndcsb  23336  2ndcsep  23346  txkgen  23539  nmoeq0  24624  nmoleub3  25019  ivth  25355  ivthle  25357  ivthle2  25358  ovolunlem1  25398  ovolicc2  25423  volivth  25508  mbfinf  25566  itg2splitlem  25649  rollelem  25893  rolle  25894  tdeglem4  25965  mdeglt  25970  deg1leb  26000  deg1lt  26002  fta1g  26075  ig1peu  26080  ig1pval3  26083  dgrle  26148  0dgrb  26151  dgreq0  26171  fta1lem  26215  fta1  26216  aannenlem1  26236  aannenlem2  26237  aalioulem2  26241  reeff1o  26357  eflogeq  26511  argregt0  26519  argrege0  26520  efopn  26567  asinsinb  26807  acoscosb  26808  atantanb  26834  musum  27101  dchrptlem1  27175  dchrptlem2  27176  lgsquadlem1  27291  nosupcbv  27614  nosupfv  27618  noinfcbv  27629  noinffv  27633  nocvxmin  27690  scutbday  27716  eqscut  27717  scutun12  27722  scutbdaylt  27730  cuteq0  27744  onsiso  28169  bdayn0sf1o  28259  dfnns2  28261  znegscl  28280  renegscl  28349  istrkgl  28385  mirreu  28591  israg  28624  lmireu  28717  lmieq  28718  gropd  28958  grstructd  28959  umgredg2  29027  umgrbi  29028  umgrnloopv  29033  umgredgprv  29034  edgumgr  29062  numedglnl  29071  umgredgnlp  29074  edgusgr  29087  usgruspgrb  29110  uhgr2edg  29135  usgredg2v  29154  ushgredgedgloop  29158  usgr1e  29172  usgrexmplef  29186  subumgredg2  29212  umgrreslem  29232  cusgrexilem2  29369  cusgrexg  29371  fusgrn0degnn0  29427  umgr2v2e  29453  vdiscusgr  29459  rusgr1vtxlem  29515  rgrusgrprc  29517  wlkon2n0  29594  upgrwlkdvdelem  29666  spthonepeq  29682  usgr2wlkneq  29686  iswwlksn  29768  wwlksnon  29781  wwlksn0  29793  wlkiswwlksupgr2  29807  wlknwwlksnbij  29818  wwlksnextbi  29824  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextbij  29832  2pthon3v  29873  umgr2wlk  29879  rusgrnumwwlkb0  29901  isclwwlkn  29956  clwwlkn1loopb  29972  hashecclwwlkn1  30006  s2elclwwlknon2  30033  uhgr3cyclex  30111  frgrwopreglem4a  30239  frgrwopreglem3  30243  frgrwopreglem5lem  30249  frgrwopreglem5  30250  frgrregorufr0  30253  friendshipgt3  30327  nvz  30598  nmlno0i  30723  norm1exi  31179  pjoc1  31363  pjoc2  31368  pj11  31643  elnlfn  31857  nmlnop0  31927  adjbd1o  32014  strlem1  32179  stcltr1i  32203  2ndimaxp  32570  fnpreimac  32595  indf1ofs  32789  isarchi  33136  ply1dg1rt  33548  minplyval  33695  qtophaus  33826  locfinreflem  33830  rhmpreimacn  33875  isrrext  33990  eulerpartlemsv3  34352  eulerpartlemgvv  34367  ballotlemelo  34479  ballotlemfmpn  34486  ballotlemiex  34493  ballotlemi1  34494  ballotlemii  34495  ballotlemfrcn0  34521  ballotlemirc  34523  bnj229  34874  bnj517  34875  bnj590  34900  bnj1097  34971  bnj1118  34974  bnj1128  34980  bnj1145  34983  f1resfz0f1d  35101  loop1cycl  35124  umgr2cycl  35128  subfacp1lem3  35169  cvmlift3lem5  35310  satffunlem1lem1  35389  satffunlem2lem1  35391  satffunlem2lem2  35393  mthmi  35564  rankeq1o  36159  weiunfr  36455  finxpreclem6  37384  poimirlem13  37627  poimirlem14  37628  poimirlem17  37631  poimirlem18  37632  poimirlem21  37635  poimirlem27  37641  poimirlem28  37642  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  lfl1  39063  lshpkrex  39111  cdleme50rnlem  40538  dochkr1  41472  dochkr1OLDN  41473  lcfrlem28  41564  mapd1o  41642  hdmap1vallem  41791  aks6d1c4  42112  hashnexinjle  42117  sticksstones2  42135  sticksstones3  42136  aks6d1c6lem3  42160  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem3  42185  unitscyglem4  42186  unitscyglem5  42187  diophrw  42747  eldioph3  42754  diophin  42760  eq0rabdioph  42764  eldioph4b  42799  fphpdo  42805  fnwe2lem2  43040  fnwe2lem3  43041  islssfgi  43061  hbt  43119  dgraaval  43133  dgraalem  43134  dgraaub  43137  mpaaeu  43139  mpaaval  43140  mpaalem  43141  rngunsnply  43158  idomsubgmo  43182  proot1mul  43183  cantnfresb  43313  fvelrnbf  45012  wessf1ornlem  45179  sumnnodd  45628  fourierdlem2  46107  fourierdlem3  46108  fcoresf1  47070  uniimafveqt  47382  elsetpreimafvrab  47395  prpair  47502  prproropf1olem1  47504  pairreueq  47511  paireqne  47512  prprspr2  47519  reuprpr  47524  requad2  47624  cycldlenngric  47928  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933  clnbgrgrim  47934  usgrgrtrirex  47949  stgrusgra  47958  uspgrlimlem1  47987  uspgrlimlem2  47988  grlimgrtri  47995  usgrexmpl1lem  48012  usgrexmpl2lem  48017  gpgusgralem  48047  gpgprismgr4cyclex  48097  uspgrsprfo  48136  ply1mulgsumlem2  48376  lindslinindsimp1  48446  snlindsntor  48460  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  nn0sumshdig  48612  istermc  49463