Theorem fveqeq2 6853

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ‘cfv 6502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510

This theorem is referenced by:  fvelimad  6911  dff13f  7213  f1veqaeq  7214  f1elima  7221  fpropnf1  7225  nf1const  7262  oteqimp  7964  fimaproj  8089  suppfnss  8143  suppssfv  8156  tz7.48lem  8384  seqomlem1  8393  seqomlem2  8394  fofinf1o  9246  fipreima  9272  cantnfp1lem3  9603  brttrcl2  9637  ssttrcl  9638  ttrcltr  9639  tcrank  9810  updjudhcoinlf  9858  updjudhcoinrg  9859  pm54.43lem  9926  ackbij1lem18  10160  ackbij1  10161  axcc2  10361  iunfo  10463  grur1  10745  injresinjlem  13720  injresinj  13721  suppssfz  13931  seqid2  13985  hashrabsn01  14310  hashrabsn1  14311  hashimarni  14378  hashbclem  14389  hashbc  14390  hash2exprb  14408  elss2prb  14425  hash2sspr  14426  hash3tpde  14430  fi1uzind  14444  brfi1indALT  14447  wrdmap  14483  wrdl1s1  14552  wrdind  14659  wrd2ind  14660  reuccatpfxs1lem  14683  reuccatpfxs1  14684  cshf1  14747  cshw1  14759  wwlktovf  14893  wwlktovf1  14894  wwlktovfo  14895  wrd2f1tovbij  14897  wrdl3s3  14899  abs1m  15273  sumrblem  15648  fsumcvg  15649  summolem2a  15652  incexc2  15775  ntrivcvgfvn0  15836  prodrblem  15866  fprodcvg  15867  prodmolem2a  15871  smupvallem  16424  smu01lem  16426  algfx  16521  iserodd  16777  prmreclem2  16859  prmreclem3  16860  vdwlem2  16924  vdwlem6  16928  vdwlem8  16930  hashbcval  16944  ramub1lem1  16968  ramub1lem2  16969  imasleval  17476  eldmcoa  18003  coaval  18006  ghmf1  19192  ghmqusnsglem1  19226  ghmquskerlem1  19229  orbsta  19259  symgextf1  19367  psgnunilem2  19441  psgnunilem3  19442  psgnunilem4  19443  odeq1  19506  odngen  19523  sylow1lem2  19545  sylow1lem4  19547  sylow1lem5  19548  pgpfi  19551  efgtlen  19672  efgsfo  19685  efgredlemd  19690  efgred  19694  gsummptnn0fzfv  19933  isabvd  20762  abveq0  20768  abvdom  20780  islbs  21045  isobs  21692  cply1mul  22257  mdetunilem1  22573  mdetunilem4  22576  mdetunilem8  22580  mdetunilem9  22581  pmatcoe1fsupp  22662  m2cpminvid2lem  22715  mp2pm2mplem4  22770  2ndci  23409  2ndcsb  23410  2ndcsep  23420  txkgen  23613  nmoeq0  24697  nmoleub3  25092  ivth  25428  ivthle  25430  ivthle2  25431  ovolunlem1  25471  ovolicc2  25496  volivth  25581  mbfinf  25639  itg2splitlem  25722  rollelem  25966  rolle  25967  tdeglem4  26038  mdeglt  26043  deg1leb  26073  deg1lt  26075  fta1g  26148  ig1peu  26153  ig1pval3  26156  dgrle  26221  0dgrb  26224  dgreq0  26244  fta1lem  26288  fta1  26289  aannenlem1  26309  aannenlem2  26310  aalioulem2  26314  reeff1o  26430  eflogeq  26584  argregt0  26592  argrege0  26593  efopn  26640  asinsinb  26880  acoscosb  26881  atantanb  26907  musum  27174  dchrptlem1  27248  dchrptlem2  27249  lgsquadlem1  27364  nosupcbv  27687  nosupfv  27691  noinfcbv  27702  noinffv  27706  nocvxmin  27768  cutbday  27797  eqcuts  27798  cutsun12  27803  cutbdaylt  27811  cuteq0  27828  negleft  28071  negright  28072  oniso  28284  bdayn0sf1o  28383  dfnns2  28385  znegscl  28405  renegscl  28511  istrkgl  28547  mirreu  28754  israg  28787  lmireu  28880  lmieq  28881  gropd  29122  grstructd  29123  umgredg2  29191  umgrbi  29192  umgrnloopv  29197  umgredgprv  29198  edgumgr  29226  numedglnl  29235  umgredgnlp  29238  edgusgr  29251  usgruspgrb  29274  uhgr2edg  29299  usgredg2v  29318  ushgredgedgloop  29322  usgr1e  29336  usgrexmplef  29350  subumgredg2  29376  umgrreslem  29396  cusgrexilem2  29533  cusgrexg  29535  fusgrn0degnn0  29591  umgr2v2e  29617  vdiscusgr  29623  rusgr1vtxlem  29679  rgrusgrprc  29681  wlkon2n0  29756  upgrwlkdvdelem  29827  spthonepeq  29843  usgr2wlkneq  29847  iswwlksn  29929  wwlksnon  29942  wwlksn0  29954  wlkiswwlksupgr2  29968  wlknwwlksnbij  29979  wwlksnextbi  29985  wwlksnextfun  29989  wwlksnextinj  29990  wwlksnextbij  29993  2pthon3v  30034  umgr2wlk  30040  rusgrnumwwlkb0  30065  isclwwlkn  30120  clwwlkn1loopb  30136  hashecclwwlkn1  30170  s2elclwwlknon2  30197  uhgr3cyclex  30275  frgrwopreglem4a  30403  frgrwopreglem3  30407  frgrwopreglem5lem  30413  frgrwopreglem5  30414  frgrregorufr0  30417  friendshipgt3  30491  nvz  30763  nmlno0i  30888  norm1exi  31344  pjoc1  31528  pjoc2  31533  pj11  31808  elnlfn  32022  nmlnop0  32092  adjbd1o  32179  strlem1  32344  stcltr1i  32368  2ndimaxp  32742  fnpreimac  32766  indf1ofs  32965  isarchi  33282  ply1dg1rt  33679  extvfval  33715  esplyfval0  33747  esplymhp  33751  esplyfv1  33752  vieta  33763  minplyval  33889  qtophaus  34020  locfinreflem  34024  rhmpreimacn  34069  isrrext  34184  eulerpartlemsv3  34545  eulerpartlemgvv  34560  ballotlemelo  34672  ballotlemfmpn  34679  ballotlemiex  34686  ballotlemi1  34687  ballotlemii  34688  ballotlemfrcn0  34714  ballotlemirc  34716  bnj229  35066  bnj517  35067  bnj590  35092  bnj1097  35163  bnj1118  35166  bnj1128  35172  bnj1145  35175  f1resfz0f1d  35336  loop1cycl  35359  umgr2cycl  35363  subfacp1lem3  35404  cvmlift3lem5  35545  satffunlem1lem1  35624  satffunlem2lem1  35626  satffunlem2lem2  35628  mthmi  35799  rankeq1o  36393  weiunfr  36689  finxpreclem6  37678  poimirlem13  37913  poimirlem14  37914  poimirlem17  37917  poimirlem18  37918  poimirlem21  37921  poimirlem27  37927  poimirlem28  37928  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  lfl1  39475  lshpkrex  39523  cdleme50rnlem  40949  dochkr1  41883  dochkr1OLDN  41884  lcfrlem28  41975  mapd1o  42053  hdmap1vallem  42202  aks6d1c4  42523  hashnexinjle  42528  sticksstones2  42546  sticksstones3  42547  aks6d1c6lem3  42571  aks6d1c6isolem1  42573  aks6d1c6isolem2  42574  grpods  42593  unitscyglem1  42594  unitscyglem2  42595  unitscyglem3  42596  unitscyglem4  42597  unitscyglem5  42598  diophrw  43145  eldioph3  43152  diophin  43158  eq0rabdioph  43162  eldioph4b  43197  fphpdo  43203  fnwe2lem2  43437  fnwe2lem3  43438  islssfgi  43458  hbt  43516  dgraaval  43530  dgraalem  43531  dgraaub  43534  mpaaeu  43536  mpaaval  43537  mpaalem  43538  rngunsnply  43555  idomsubgmo  43579  proot1mul  43580  cantnfresb  43710  fvelrnbf  45407  wessf1ornlem  45573  sumnnodd  46019  fourierdlem2  46496  fourierdlem3  46497  fcoresf1  47458  uniimafveqt  47770  elsetpreimafvrab  47783  prpair  47890  prproropf1olem1  47892  pairreueq  47899  paireqne  47900  prprspr2  47907  reuprpr  47912  requad2  48012  cycldlenngric  48317  uhgrimisgrgriclem  48319  clnbgrgrimlem  48322  clnbgrgrim  48323  usgrgrtrirex  48339  stgrusgra  48348  uspgrlimlem1  48377  uspgrlimlem2  48378  grlimgrtri  48392  usgrexmpl1lem  48410  usgrexmpl2lem  48415  gpgusgralem  48445  gpgprismgr4cyclex  48496  uspgrsprfo  48537  ply1mulgsumlem2  48776  lindslinindsimp1  48846  snlindsntor  48860  nn0sumshdiglemA  49008  nn0sumshdiglemB  49009  nn0sumshdiglem1  49010  nn0sumshdig  49012  istermc  49862