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 1540  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569

This theorem is referenced by:  fvelimad  6976  dff13f  7276  f1veqaeq  7277  f1elima  7283  fpropnf1  7287  nf1const  7324  oteqimp  8033  fimaproj  8160  suppfnss  8214  suppssfv  8227  tz7.48lem  8481  seqomlem1  8490  seqomlem2  8491  fofinf1o  9372  fipreima  9398  cantnfp1lem3  9720  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  tcrank  9924  updjudhcoinlf  9972  updjudhcoinrg  9973  pm54.43lem  10040  ackbij1lem18  10276  ackbij1  10277  axcc2  10477  iunfo  10579  grur1  10860  injresinjlem  13826  injresinj  13827  suppssfz  14035  seqid2  14089  hashrabsn01  14412  hashrabsn1  14413  hashimarni  14480  hashbclem  14491  hashbc  14492  hash2exprb  14510  elss2prb  14527  hash2sspr  14528  hash3tpde  14532  fi1uzind  14546  brfi1indALT  14549  wrdmap  14584  wrdl1s1  14652  wrdind  14760  wrd2ind  14761  reuccatpfxs1lem  14784  reuccatpfxs1  14785  cshf1  14848  cshw1  14860  wwlktovf  14995  wwlktovf1  14996  wwlktovfo  14997  wrd2f1tovbij  14999  wrdl3s3  15001  abs1m  15374  sumrblem  15747  fsumcvg  15748  summolem2a  15751  incexc2  15874  ntrivcvgfvn0  15935  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  smupvallem  16520  smu01lem  16522  algfx  16617  iserodd  16873  prmreclem2  16955  prmreclem3  16956  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  hashbcval  17040  ramub1lem1  17064  ramub1lem2  17065  imasleval  17586  eldmcoa  18110  coaval  18113  ghmf1  19264  ghmqusnsglem1  19298  ghmquskerlem1  19301  orbsta  19331  symgextf1  19439  psgnunilem2  19513  psgnunilem3  19514  psgnunilem4  19515  odeq1  19578  odngen  19595  sylow1lem2  19617  sylow1lem4  19619  sylow1lem5  19620  pgpfi  19623  efgtlen  19744  efgsfo  19757  efgredlemd  19762  efgred  19766  gsummptnn0fzfv  20005  isabvd  20813  abveq0  20819  abvdom  20831  islbs  21075  isobs  21740  cply1mul  22300  mdetunilem1  22618  mdetunilem4  22621  mdetunilem8  22625  mdetunilem9  22626  pmatcoe1fsupp  22707  m2cpminvid2lem  22760  mp2pm2mplem4  22815  2ndci  23456  2ndcsb  23457  2ndcsep  23467  txkgen  23660  nmoeq0  24757  nmoleub3  25152  ivth  25489  ivthle  25491  ivthle2  25492  ovolunlem1  25532  ovolicc2  25557  volivth  25642  mbfinf  25700  itg2splitlem  25783  rollelem  26027  rolle  26028  tdeglem4  26099  mdeglt  26104  deg1leb  26134  deg1lt  26136  fta1g  26209  ig1peu  26214  ig1pval3  26217  dgrle  26282  0dgrb  26285  dgreq0  26305  fta1lem  26349  fta1  26350  aannenlem1  26370  aannenlem2  26371  aalioulem2  26375  reeff1o  26491  eflogeq  26644  argregt0  26652  argrege0  26653  efopn  26700  asinsinb  26940  acoscosb  26941  atantanb  26967  musum  27234  dchrptlem1  27308  dchrptlem2  27309  lgsquadlem1  27424  nosupcbv  27747  nosupfv  27751  noinfcbv  27762  noinffv  27766  nocvxmin  27823  scutbday  27849  eqscut  27850  scutun12  27855  scutbdaylt  27863  cuteq0  27877  dfnns2  28362  znegscl  28378  renegscl  28430  istrkgl  28466  mirreu  28672  israg  28705  lmireu  28798  lmieq  28799  gropd  29048  grstructd  29049  umgredg2  29117  umgrbi  29118  umgrnloopv  29123  umgredgprv  29124  edgumgr  29152  numedglnl  29161  umgredgnlp  29164  edgusgr  29177  usgruspgrb  29200  uhgr2edg  29225  usgredg2v  29244  ushgredgedgloop  29248  usgr1e  29262  usgrexmplef  29276  subumgredg2  29302  umgrreslem  29322  cusgrexilem2  29459  cusgrexg  29461  fusgrn0degnn0  29517  umgr2v2e  29543  vdiscusgr  29549  rusgr1vtxlem  29605  rgrusgrprc  29607  wlkon2n0  29684  upgrwlkdvdelem  29756  spthonepeq  29772  usgr2wlkneq  29776  iswwlksn  29858  wwlksnon  29871  wwlksn0  29883  wlkiswwlksupgr2  29897  wlknwwlksnbij  29908  wwlksnextbi  29914  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextbij  29922  2pthon3v  29963  umgr2wlk  29969  rusgrnumwwlkb0  29991  isclwwlkn  30046  clwwlkn1loopb  30062  hashecclwwlkn1  30096  s2elclwwlknon2  30123  uhgr3cyclex  30201  frgrwopreglem4a  30329  frgrwopreglem3  30333  frgrwopreglem5lem  30339  frgrwopreglem5  30340  frgrregorufr0  30343  friendshipgt3  30417  nvz  30688  nmlno0i  30813  norm1exi  31269  pjoc1  31453  pjoc2  31458  pj11  31733  elnlfn  31947  nmlnop0  32017  adjbd1o  32104  strlem1  32269  stcltr1i  32293  2ndimaxp  32656  fnpreimac  32681  indf1ofs  32851  isarchi  33189  ply1dg1rt  33604  minplyval  33748  qtophaus  33835  locfinreflem  33839  rhmpreimacn  33884  isrrext  34001  eulerpartlemsv3  34363  eulerpartlemgvv  34378  ballotlemelo  34490  ballotlemfmpn  34497  ballotlemiex  34504  ballotlemi1  34505  ballotlemii  34506  ballotlemfrcn0  34532  ballotlemirc  34534  bnj229  34898  bnj517  34899  bnj590  34924  bnj1097  34995  bnj1118  34998  bnj1128  35004  bnj1145  35007  f1resfz0f1d  35119  loop1cycl  35142  umgr2cycl  35146  subfacp1lem3  35187  cvmlift3lem5  35328  satffunlem1lem1  35407  satffunlem2lem1  35409  satffunlem2lem2  35411  mthmi  35582  rankeq1o  36172  weiunfr  36468  finxpreclem6  37397  poimirlem13  37640  poimirlem14  37641  poimirlem17  37644  poimirlem18  37645  poimirlem21  37648  poimirlem27  37654  poimirlem28  37655  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  lfl1  39071  lshpkrex  39119  cdleme50rnlem  40546  dochkr1  41480  dochkr1OLDN  41481  lcfrlem28  41572  mapd1o  41650  hdmap1vallem  41799  aks6d1c4  42125  hashnexinjle  42130  sticksstones2  42148  sticksstones3  42149  aks6d1c6lem3  42173  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem3  42198  unitscyglem4  42199  unitscyglem5  42200  diophrw  42770  eldioph3  42777  diophin  42783  eq0rabdioph  42787  eldioph4b  42822  fphpdo  42828  fnwe2lem2  43063  fnwe2lem3  43064  islssfgi  43084  hbt  43142  dgraaval  43156  dgraalem  43157  dgraaub  43160  mpaaeu  43162  mpaaval  43163  mpaalem  43164  rngunsnply  43181  idomsubgmo  43205  proot1mul  43206  cantnfresb  43337  fvelrnbf  45023  wessf1ornlem  45190  sumnnodd  45645  fourierdlem2  46124  fourierdlem3  46125  fcoresf1  47081  uniimafveqt  47368  elsetpreimafvrab  47381  prpair  47488  prproropf1olem1  47490  pairreueq  47497  paireqne  47498  prprspr2  47505  reuprpr  47510  requad2  47610  uhgrimisgrgriclem  47898  clnbgrgrimlem  47901  clnbgrgrim  47902  usgrgrtrirex  47917  stgrusgra  47926  uspgrlimlem1  47955  uspgrlimlem2  47956  grlimgrtri  47963  usgrexmpl1lem  47980  usgrexmpl2lem  47985  gpgusgralem  48011  uspgrsprfo  48064  ply1mulgsumlem2  48304  lindslinindsimp1  48374  snlindsntor  48388  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  nn0sumshdig  48544  istermc  49121