Theorem fveqeq2 6679

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  fvelimad  6732  dff13f  7014  f1veqaeq  7015  f1elima  7021  fpropnf1  7025  nf1const  7059  oteqimp  7708  fimaproj  7829  suppfnss  7855  suppssfv  7866  tz7.48lem  8077  seqomlem1  8086  seqomlem2  8087  fofinf1o  8799  fipreima  8830  cantnfp1lem3  9143  tcrank  9313  updjudhcoinlf  9361  updjudhcoinrg  9362  pm54.43lem  9428  ackbij1lem18  9659  ackbij1  9660  axcc2  9859  iunfo  9961  grur1  10242  injresinjlem  13158  injresinj  13159  suppssfz  13363  seqid2  13417  hashrabsn01  13735  hashrabsn1  13736  hashimarni  13803  hashbclem  13811  hashbc  13812  hash2exprb  13830  elss2prb  13846  hash2sspr  13847  fi1uzind  13856  wrdmap  13897  wrdl1s1  13968  wrdind  14084  wrd2ind  14085  reuccatpfxs1lem  14108  reuccatpfxs1  14109  cshf1  14172  cshw1  14184  wwlktovf  14320  wwlktovf1  14321  wwlktovfo  14322  wrd2f1tovbij  14324  wrdl3s3  14326  abs1m  14695  sumrblem  15068  fsumcvg  15069  summolem2a  15072  incexc2  15193  ntrivcvgfvn0  15255  prodrblem  15283  fprodcvg  15284  prodmolem2a  15288  smupvallem  15832  smu01lem  15834  algfx  15924  iserodd  16172  prmreclem2  16253  prmreclem3  16254  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  hashbcval  16338  ramub1lem1  16362  ramub1lem2  16363  imasleval  16814  eldmcoa  17325  coaval  17328  ghmf1  18387  orbsta  18443  symgextf1  18549  psgnunilem2  18623  psgnunilem3  18624  psgnunilem4  18625  odeq1  18687  odngen  18702  sylow1lem2  18724  sylow1lem4  18726  sylow1lem5  18727  pgpfi  18730  efgtlen  18852  efgsfo  18865  efgredlemd  18870  efgred  18874  gsummptnn0fzfv  19107  isabvd  19591  abveq0  19597  abvdom  19609  islbs  19848  cply1mul  20462  isobs  20864  mdetunilem1  21221  mdetunilem4  21224  mdetunilem8  21228  mdetunilem9  21229  pmatcoe1fsupp  21309  m2cpminvid2lem  21362  mp2pm2mplem4  21417  2ndci  22056  2ndcsb  22057  2ndcsep  22067  txkgen  22260  nmoeq0  23345  nmoleub3  23723  ivth  24055  ivthle  24057  ivthle2  24058  ovolunlem1  24098  ovolicc2  24123  volivth  24208  mbfinf  24266  itg2splitlem  24349  rollelem  24586  rolle  24587  tdeglem4  24654  mdeglt  24659  deg1leb  24689  deg1lt  24691  fta1g  24761  ig1peu  24765  ig1pval3  24768  dgrle  24833  0dgrb  24836  dgreq0  24855  fta1lem  24896  fta1  24897  aannenlem1  24917  aannenlem2  24918  aalioulem2  24922  reeff1o  25035  eflogeq  25185  argregt0  25193  argrege0  25194  efopn  25241  asinsinb  25475  acoscosb  25476  atantanb  25502  musum  25768  dchrptlem1  25840  dchrptlem2  25841  lgsquadlem1  25956  istrkgl  26244  mirreu  26450  israg  26483  lmireu  26576  lmieq  26577  gropd  26816  grstructd  26817  umgredg2  26885  umgrbi  26886  umgrnloopv  26891  umgredgprv  26892  edgumgr  26920  numedglnl  26929  umgredgnlp  26932  edgusgr  26945  usgruspgrb  26966  uhgr2edg  26990  usgredg2v  27009  ushgredgedgloop  27013  usgr1e  27027  usgrexmplef  27041  subumgredg2  27067  umgrreslem  27087  cusgrexilem2  27224  cusgrexg  27226  fusgrn0degnn0  27281  umgr2v2e  27307  vdiscusgr  27313  rusgr1vtxlem  27369  rgrusgrprc  27371  wlkon2n0  27448  upgrwlkdvdelem  27517  spthonepeq  27533  usgr2wlkneq  27537  iswwlksn  27616  wwlksnon  27629  wwlksn0  27641  wlkiswwlksupgr2  27655  wlknwwlksnbij  27666  wwlksnextbi  27672  wwlksnextfun  27676  wwlksnextinj  27677  wwlksnextbij  27680  2pthon3v  27722  umgr2wlk  27728  rusgrnumwwlkb0  27750  isclwwlkn  27805  clwwlkn1loopb  27821  hashecclwwlkn1  27856  s2elclwwlknon2  27883  uhgr3cyclex  27961  frgrwopreglem4a  28089  frgrwopreglem3  28093  frgrwopreglem5lem  28099  frgrwopreglem5  28100  frgrregorufr0  28103  friendshipgt3  28177  nvz  28446  nmlno0i  28571  norm1exi  29027  pjoc1  29211  pjoc2  29216  pj11  29491  elnlfn  29705  nmlnop0  29775  adjbd1o  29862  strlem1  30027  stcltr1i  30051  fnpreimac  30416  isarchi  30811  qtophaus  31100  locfinreflem  31104  isrrext  31241  indf1ofs  31285  eulerpartlemsv3  31619  eulerpartlemgvv  31634  ballotlemelo  31745  ballotlemfmpn  31752  ballotlemiex  31759  ballotlemi1  31760  ballotlemii  31761  ballotlemfrcn0  31787  ballotlemirc  31789  bnj229  32156  bnj517  32157  bnj590  32182  bnj1097  32253  bnj1118  32256  bnj1128  32262  bnj1145  32265  f1resfz0f1d  32361  loop1cycl  32384  umgr2cycl  32388  subfacp1lem3  32429  cvmlift3lem5  32570  satffunlem1lem1  32649  satffunlem2lem1  32651  satffunlem2lem2  32653  mthmi  32824  trpred0  33075  nosupfv  33206  noeta  33222  nocvxmin  33248  scutbday  33267  scutun12  33271  scutbdaylt  33276  rankeq1o  33632  finxpreclem6  34680  poimirlem13  34920  poimirlem14  34921  poimirlem17  34924  poimirlem18  34925  poimirlem21  34928  poimirlem27  34934  poimirlem28  34935  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  lfl1  36221  lshpkrex  36269  cdleme50rnlem  37695  dochkr1  38629  dochkr1OLDN  38630  lcfrlem28  38721  mapd1o  38799  hdmap1vallem  38948  diophrw  39405  eldioph3  39412  diophin  39418  eq0rabdioph  39422  eldioph4b  39457  fphpdo  39463  fnwe2lem2  39700  fnwe2lem3  39701  islssfgi  39721  hbt  39779  dgraaval  39793  dgraalem  39794  dgraaub  39797  mpaaeu  39799  mpaaval  39800  mpaalem  39801  rngunsnply  39822  idomsubgmo  39847  proot1mul  39848  fvelrnbf  41324  wessf1ornlem  41494  sumnnodd  41960  fourierdlem2  42443  fourierdlem3  42444  uniimafveqt  43590  elsetpreimafvrab  43603  prpair  43712  prproropf1olem1  43714  pairreueq  43721  paireqne  43722  prprspr2  43729  reuprpr  43734  requad2  43837  uspgrsprfo  44072  ply1mulgsumlem2  44490  lindslinindsimp1  44561  snlindsntor  44575  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  nn0sumshdiglem1  44730  nn0sumshdig  44732