Theorem fveqeq2 6870

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522

This theorem is referenced by:  fvelimad  6931  dff13f  7233  f1veqaeq  7234  f1elima  7241  fpropnf1  7245  nf1const  7282  oteqimp  7990  fimaproj  8117  suppfnss  8171  suppssfv  8184  tz7.48lem  8412  seqomlem1  8421  seqomlem2  8422  fofinf1o  9290  fipreima  9316  cantnfp1lem3  9640  brttrcl2  9674  ssttrcl  9675  ttrcltr  9676  tcrank  9844  updjudhcoinlf  9892  updjudhcoinrg  9893  pm54.43lem  9960  ackbij1lem18  10196  ackbij1  10197  axcc2  10397  iunfo  10499  grur1  10780  injresinjlem  13755  injresinj  13756  suppssfz  13966  seqid2  14020  hashrabsn01  14345  hashrabsn1  14346  hashimarni  14413  hashbclem  14424  hashbc  14425  hash2exprb  14443  elss2prb  14460  hash2sspr  14461  hash3tpde  14465  fi1uzind  14479  brfi1indALT  14482  wrdmap  14518  wrdl1s1  14586  wrdind  14694  wrd2ind  14695  reuccatpfxs1lem  14718  reuccatpfxs1  14719  cshf1  14782  cshw1  14794  wwlktovf  14929  wwlktovf1  14930  wwlktovfo  14931  wrd2f1tovbij  14933  wrdl3s3  14935  abs1m  15309  sumrblem  15684  fsumcvg  15685  summolem2a  15688  incexc2  15811  ntrivcvgfvn0  15872  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  smupvallem  16460  smu01lem  16462  algfx  16557  iserodd  16813  prmreclem2  16895  prmreclem3  16896  vdwlem2  16960  vdwlem6  16964  vdwlem8  16966  hashbcval  16980  ramub1lem1  17004  ramub1lem2  17005  imasleval  17511  eldmcoa  18034  coaval  18037  ghmf1  19185  ghmqusnsglem1  19219  ghmquskerlem1  19222  orbsta  19252  symgextf1  19358  psgnunilem2  19432  psgnunilem3  19433  psgnunilem4  19434  odeq1  19497  odngen  19514  sylow1lem2  19536  sylow1lem4  19538  sylow1lem5  19539  pgpfi  19542  efgtlen  19663  efgsfo  19676  efgredlemd  19681  efgred  19685  gsummptnn0fzfv  19924  isabvd  20728  abveq0  20734  abvdom  20746  islbs  20990  isobs  21636  cply1mul  22190  mdetunilem1  22506  mdetunilem4  22509  mdetunilem8  22513  mdetunilem9  22514  pmatcoe1fsupp  22595  m2cpminvid2lem  22648  mp2pm2mplem4  22703  2ndci  23342  2ndcsb  23343  2ndcsep  23353  txkgen  23546  nmoeq0  24631  nmoleub3  25026  ivth  25362  ivthle  25364  ivthle2  25365  ovolunlem1  25405  ovolicc2  25430  volivth  25515  mbfinf  25573  itg2splitlem  25656  rollelem  25900  rolle  25901  tdeglem4  25972  mdeglt  25977  deg1leb  26007  deg1lt  26009  fta1g  26082  ig1peu  26087  ig1pval3  26090  dgrle  26155  0dgrb  26158  dgreq0  26178  fta1lem  26222  fta1  26223  aannenlem1  26243  aannenlem2  26244  aalioulem2  26248  reeff1o  26364  eflogeq  26518  argregt0  26526  argrege0  26527  efopn  26574  asinsinb  26814  acoscosb  26815  atantanb  26841  musum  27108  dchrptlem1  27182  dchrptlem2  27183  lgsquadlem1  27298  nosupcbv  27621  nosupfv  27625  noinfcbv  27636  noinffv  27640  nocvxmin  27697  scutbday  27723  eqscut  27724  scutun12  27729  scutbdaylt  27737  cuteq0  27751  onsiso  28176  bdayn0sf1o  28266  dfnns2  28268  znegscl  28287  renegscl  28356  istrkgl  28392  mirreu  28598  israg  28631  lmireu  28724  lmieq  28725  gropd  28965  grstructd  28966  umgredg2  29034  umgrbi  29035  umgrnloopv  29040  umgredgprv  29041  edgumgr  29069  numedglnl  29078  umgredgnlp  29081  edgusgr  29094  usgruspgrb  29117  uhgr2edg  29142  usgredg2v  29161  ushgredgedgloop  29165  usgr1e  29179  usgrexmplef  29193  subumgredg2  29219  umgrreslem  29239  cusgrexilem2  29376  cusgrexg  29378  fusgrn0degnn0  29434  umgr2v2e  29460  vdiscusgr  29466  rusgr1vtxlem  29522  rgrusgrprc  29524  wlkon2n0  29601  upgrwlkdvdelem  29673  spthonepeq  29689  usgr2wlkneq  29693  iswwlksn  29775  wwlksnon  29788  wwlksn0  29800  wlkiswwlksupgr2  29814  wlknwwlksnbij  29825  wwlksnextbi  29831  wwlksnextfun  29835  wwlksnextinj  29836  wwlksnextbij  29839  2pthon3v  29880  umgr2wlk  29886  rusgrnumwwlkb0  29908  isclwwlkn  29963  clwwlkn1loopb  29979  hashecclwwlkn1  30013  s2elclwwlknon2  30040  uhgr3cyclex  30118  frgrwopreglem4a  30246  frgrwopreglem3  30250  frgrwopreglem5lem  30256  frgrwopreglem5  30257  frgrregorufr0  30260  friendshipgt3  30334  nvz  30605  nmlno0i  30730  norm1exi  31186  pjoc1  31370  pjoc2  31375  pj11  31650  elnlfn  31864  nmlnop0  31934  adjbd1o  32021  strlem1  32186  stcltr1i  32210  2ndimaxp  32577  fnpreimac  32602  indf1ofs  32796  isarchi  33143  ply1dg1rt  33555  minplyval  33702  qtophaus  33833  locfinreflem  33837  rhmpreimacn  33882  isrrext  33997  eulerpartlemsv3  34359  eulerpartlemgvv  34374  ballotlemelo  34486  ballotlemfmpn  34493  ballotlemiex  34500  ballotlemi1  34501  ballotlemii  34502  ballotlemfrcn0  34528  ballotlemirc  34530  bnj229  34881  bnj517  34882  bnj590  34907  bnj1097  34978  bnj1118  34981  bnj1128  34987  bnj1145  34990  f1resfz0f1d  35108  loop1cycl  35131  umgr2cycl  35135  subfacp1lem3  35176  cvmlift3lem5  35317  satffunlem1lem1  35396  satffunlem2lem1  35398  satffunlem2lem2  35400  mthmi  35571  rankeq1o  36166  weiunfr  36462  finxpreclem6  37391  poimirlem13  37634  poimirlem14  37635  poimirlem17  37638  poimirlem18  37639  poimirlem21  37642  poimirlem27  37648  poimirlem28  37649  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  lfl1  39070  lshpkrex  39118  cdleme50rnlem  40545  dochkr1  41479  dochkr1OLDN  41480  lcfrlem28  41571  mapd1o  41649  hdmap1vallem  41798  aks6d1c4  42119  hashnexinjle  42124  sticksstones2  42142  sticksstones3  42143  aks6d1c6lem3  42167  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem3  42192  unitscyglem4  42193  unitscyglem5  42194  diophrw  42754  eldioph3  42761  diophin  42767  eq0rabdioph  42771  eldioph4b  42806  fphpdo  42812  fnwe2lem2  43047  fnwe2lem3  43048  islssfgi  43068  hbt  43126  dgraaval  43140  dgraalem  43141  dgraaub  43144  mpaaeu  43146  mpaaval  43147  mpaalem  43148  rngunsnply  43165  idomsubgmo  43189  proot1mul  43190  cantnfresb  43320  fvelrnbf  45019  wessf1ornlem  45186  sumnnodd  45635  fourierdlem2  46114  fourierdlem3  46115  fcoresf1  47074  uniimafveqt  47386  elsetpreimafvrab  47399  prpair  47506  prproropf1olem1  47508  pairreueq  47515  paireqne  47516  prprspr2  47523  reuprpr  47528  requad2  47628  cycldlenngric  47932  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937  clnbgrgrim  47938  usgrgrtrirex  47953  stgrusgra  47962  uspgrlimlem1  47991  uspgrlimlem2  47992  grlimgrtri  47999  usgrexmpl1lem  48016  usgrexmpl2lem  48021  gpgusgralem  48051  gpgprismgr4cyclex  48101  uspgrsprfo  48140  ply1mulgsumlem2  48380  lindslinindsimp1  48450  snlindsntor  48464  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  nn0sumshdig  48616  istermc  49467