Theorem fveqeq2 6915

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570

This theorem is referenced by:  fvelimad  6975  dff13f  7275  f1veqaeq  7276  f1elima  7282  fpropnf1  7286  nf1const  7323  oteqimp  8031  fimaproj  8158  suppfnss  8212  suppssfv  8225  tz7.48lem  8479  seqomlem1  8488  seqomlem2  8489  fofinf1o  9369  fipreima  9395  cantnfp1lem3  9717  brttrcl2  9751  ssttrcl  9752  ttrcltr  9753  tcrank  9921  updjudhcoinlf  9969  updjudhcoinrg  9970  pm54.43lem  10037  ackbij1lem18  10273  ackbij1  10274  axcc2  10474  iunfo  10576  grur1  10857  injresinjlem  13822  injresinj  13823  suppssfz  14031  seqid2  14085  hashrabsn01  14408  hashrabsn1  14409  hashimarni  14476  hashbclem  14487  hashbc  14488  hash2exprb  14506  elss2prb  14523  hash2sspr  14524  hash3tpde  14528  fi1uzind  14542  brfi1indALT  14545  wrdmap  14580  wrdl1s1  14648  wrdind  14756  wrd2ind  14757  reuccatpfxs1lem  14780  reuccatpfxs1  14781  cshf1  14844  cshw1  14856  wwlktovf  14991  wwlktovf1  14992  wwlktovfo  14993  wrd2f1tovbij  14995  wrdl3s3  14997  abs1m  15370  sumrblem  15743  fsumcvg  15744  summolem2a  15747  incexc2  15870  ntrivcvgfvn0  15931  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  smupvallem  16516  smu01lem  16518  algfx  16613  iserodd  16868  prmreclem2  16950  prmreclem3  16951  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  hashbcval  17035  ramub1lem1  17059  ramub1lem2  17060  imasleval  17587  eldmcoa  18118  coaval  18121  ghmf1  19276  ghmqusnsglem1  19310  ghmquskerlem1  19313  orbsta  19343  symgextf1  19453  psgnunilem2  19527  psgnunilem3  19528  psgnunilem4  19529  odeq1  19592  odngen  19609  sylow1lem2  19631  sylow1lem4  19633  sylow1lem5  19634  pgpfi  19637  efgtlen  19758  efgsfo  19771  efgredlemd  19776  efgred  19780  gsummptnn0fzfv  20019  isabvd  20829  abveq0  20835  abvdom  20847  islbs  21092  isobs  21757  cply1mul  22315  mdetunilem1  22633  mdetunilem4  22636  mdetunilem8  22640  mdetunilem9  22641  pmatcoe1fsupp  22722  m2cpminvid2lem  22775  mp2pm2mplem4  22830  2ndci  23471  2ndcsb  23472  2ndcsep  23482  txkgen  23675  nmoeq0  24772  nmoleub3  25165  ivth  25502  ivthle  25504  ivthle2  25505  ovolunlem1  25545  ovolicc2  25570  volivth  25655  mbfinf  25713  itg2splitlem  25797  rollelem  26041  rolle  26042  tdeglem4  26113  mdeglt  26118  deg1leb  26148  deg1lt  26150  fta1g  26223  ig1peu  26228  ig1pval3  26231  dgrle  26296  0dgrb  26299  dgreq0  26319  fta1lem  26363  fta1  26364  aannenlem1  26384  aannenlem2  26385  aalioulem2  26389  reeff1o  26505  eflogeq  26658  argregt0  26666  argrege0  26667  efopn  26714  asinsinb  26954  acoscosb  26955  atantanb  26981  musum  27248  dchrptlem1  27322  dchrptlem2  27323  lgsquadlem1  27438  nosupcbv  27761  nosupfv  27765  noinfcbv  27776  noinffv  27780  nocvxmin  27837  scutbday  27863  eqscut  27864  scutun12  27869  scutbdaylt  27877  cuteq0  27891  dfnns2  28376  znegscl  28392  renegscl  28444  istrkgl  28480  mirreu  28686  israg  28719  lmireu  28812  lmieq  28813  gropd  29062  grstructd  29063  umgredg2  29131  umgrbi  29132  umgrnloopv  29137  umgredgprv  29138  edgumgr  29166  numedglnl  29175  umgredgnlp  29178  edgusgr  29191  usgruspgrb  29214  uhgr2edg  29239  usgredg2v  29258  ushgredgedgloop  29262  usgr1e  29276  usgrexmplef  29290  subumgredg2  29316  umgrreslem  29336  cusgrexilem2  29473  cusgrexg  29475  fusgrn0degnn0  29531  umgr2v2e  29557  vdiscusgr  29563  rusgr1vtxlem  29619  rgrusgrprc  29621  wlkon2n0  29698  upgrwlkdvdelem  29768  spthonepeq  29784  usgr2wlkneq  29788  iswwlksn  29867  wwlksnon  29880  wwlksn0  29892  wlkiswwlksupgr2  29906  wlknwwlksnbij  29917  wwlksnextbi  29923  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextbij  29931  2pthon3v  29972  umgr2wlk  29978  rusgrnumwwlkb0  30000  isclwwlkn  30055  clwwlkn1loopb  30071  hashecclwwlkn1  30105  s2elclwwlknon2  30132  uhgr3cyclex  30210  frgrwopreglem4a  30338  frgrwopreglem3  30342  frgrwopreglem5lem  30348  frgrwopreglem5  30349  frgrregorufr0  30352  friendshipgt3  30426  nvz  30697  nmlno0i  30822  norm1exi  31278  pjoc1  31462  pjoc2  31467  pj11  31742  elnlfn  31956  nmlnop0  32026  adjbd1o  32113  strlem1  32278  stcltr1i  32302  2ndimaxp  32662  fnpreimac  32687  isarchi  33171  ply1dg1rt  33583  minplyval  33712  qtophaus  33796  locfinreflem  33800  rhmpreimacn  33845  isrrext  33962  indf1ofs  34006  eulerpartlemsv3  34342  eulerpartlemgvv  34357  ballotlemelo  34468  ballotlemfmpn  34475  ballotlemiex  34482  ballotlemi1  34483  ballotlemii  34484  ballotlemfrcn0  34510  ballotlemirc  34512  bnj229  34876  bnj517  34877  bnj590  34902  bnj1097  34973  bnj1118  34976  bnj1128  34982  bnj1145  34985  f1resfz0f1d  35097  loop1cycl  35121  umgr2cycl  35125  subfacp1lem3  35166  cvmlift3lem5  35307  satffunlem1lem1  35386  satffunlem2lem1  35388  satffunlem2lem2  35390  mthmi  35561  rankeq1o  36152  weiunfr  36449  finxpreclem6  37378  poimirlem13  37619  poimirlem14  37620  poimirlem17  37623  poimirlem18  37624  poimirlem21  37627  poimirlem27  37633  poimirlem28  37634  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  lfl1  39051  lshpkrex  39099  cdleme50rnlem  40526  dochkr1  41460  dochkr1OLDN  41461  lcfrlem28  41552  mapd1o  41630  hdmap1vallem  41779  aks6d1c4  42105  hashnexinjle  42110  sticksstones2  42128  sticksstones3  42129  aks6d1c6lem3  42153  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  unitscyglem5  42180  diophrw  42746  eldioph3  42753  diophin  42759  eq0rabdioph  42763  eldioph4b  42798  fphpdo  42804  fnwe2lem2  43039  fnwe2lem3  43040  islssfgi  43060  hbt  43118  dgraaval  43132  dgraalem  43133  dgraaub  43136  mpaaeu  43138  mpaaval  43139  mpaalem  43140  rngunsnply  43157  idomsubgmo  43181  proot1mul  43182  cantnfresb  43313  fvelrnbf  44955  wessf1ornlem  45127  sumnnodd  45585  fourierdlem2  46064  fourierdlem3  46065  fcoresf1  47018  uniimafveqt  47305  elsetpreimafvrab  47318  prpair  47425  prproropf1olem1  47427  pairreueq  47434  paireqne  47435  prprspr2  47442  reuprpr  47447  requad2  47547  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838  clnbgrgrim  47839  usgrgrtrirex  47852  stgrusgra  47861  uspgrlimlem1  47890  uspgrlimlem2  47891  grlimgrtri  47898  usgrexmpl1lem  47915  usgrexmpl2lem  47920  gpgusgralem  47945  uspgrsprfo  47991  ply1mulgsumlem2  48232  lindslinindsimp1  48302  snlindsntor  48316  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  nn0sumshdig  48472