Theorem fveqeq2 6929

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  fvelimad  6989  dff13f  7293  f1veqaeq  7294  f1elima  7300  fpropnf1  7304  nf1const  7340  oteqimp  8049  fimaproj  8176  suppfnss  8230  suppssfv  8243  tz7.48lem  8497  seqomlem1  8506  seqomlem2  8507  fofinf1o  9400  fipreima  9428  cantnfp1lem3  9749  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  tcrank  9953  updjudhcoinlf  10001  updjudhcoinrg  10002  pm54.43lem  10069  ackbij1lem18  10305  ackbij1  10306  axcc2  10506  iunfo  10608  grur1  10889  injresinjlem  13837  injresinj  13838  suppssfz  14045  seqid2  14099  hashrabsn01  14422  hashrabsn1  14423  hashimarni  14490  hashbclem  14501  hashbc  14502  hash2exprb  14520  elss2prb  14537  hash2sspr  14538  hash3tpde  14542  fi1uzind  14556  brfi1indALT  14559  wrdmap  14594  wrdl1s1  14662  wrdind  14770  wrd2ind  14771  reuccatpfxs1lem  14794  reuccatpfxs1  14795  cshf1  14858  cshw1  14870  wwlktovf  15005  wwlktovf1  15006  wwlktovfo  15007  wrd2f1tovbij  15009  wrdl3s3  15011  abs1m  15384  sumrblem  15759  fsumcvg  15760  summolem2a  15763  incexc2  15886  ntrivcvgfvn0  15947  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  smupvallem  16529  smu01lem  16531  algfx  16627  iserodd  16882  prmreclem2  16964  prmreclem3  16965  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  hashbcval  17049  ramub1lem1  17073  ramub1lem2  17074  imasleval  17601  eldmcoa  18132  coaval  18135  ghmf1  19286  ghmqusnsglem1  19320  ghmquskerlem1  19323  orbsta  19353  symgextf1  19463  psgnunilem2  19537  psgnunilem3  19538  psgnunilem4  19539  odeq1  19602  odngen  19619  sylow1lem2  19641  sylow1lem4  19643  sylow1lem5  19644  pgpfi  19647  efgtlen  19768  efgsfo  19781  efgredlemd  19786  efgred  19790  gsummptnn0fzfv  20029  isabvd  20835  abveq0  20841  abvdom  20853  islbs  21098  isobs  21763  cply1mul  22321  mdetunilem1  22639  mdetunilem4  22642  mdetunilem8  22646  mdetunilem9  22647  pmatcoe1fsupp  22728  m2cpminvid2lem  22781  mp2pm2mplem4  22836  2ndci  23477  2ndcsb  23478  2ndcsep  23488  txkgen  23681  nmoeq0  24778  nmoleub3  25171  ivth  25508  ivthle  25510  ivthle2  25511  ovolunlem1  25551  ovolicc2  25576  volivth  25661  mbfinf  25719  itg2splitlem  25803  rollelem  26047  rolle  26048  tdeglem4  26119  mdeglt  26124  deg1leb  26154  deg1lt  26156  fta1g  26229  ig1peu  26234  ig1pval3  26237  dgrle  26302  0dgrb  26305  dgreq0  26325  fta1lem  26367  fta1  26368  aannenlem1  26388  aannenlem2  26389  aalioulem2  26393  reeff1o  26509  eflogeq  26662  argregt0  26670  argrege0  26671  efopn  26718  asinsinb  26958  acoscosb  26959  atantanb  26985  musum  27252  dchrptlem1  27326  dchrptlem2  27327  lgsquadlem1  27442  nosupcbv  27765  nosupfv  27769  noinfcbv  27780  noinffv  27784  nocvxmin  27841  scutbday  27867  eqscut  27868  scutun12  27873  scutbdaylt  27881  cuteq0  27895  dfnns2  28380  znegscl  28396  renegscl  28448  istrkgl  28484  mirreu  28690  israg  28723  lmireu  28816  lmieq  28817  gropd  29066  grstructd  29067  umgredg2  29135  umgrbi  29136  umgrnloopv  29141  umgredgprv  29142  edgumgr  29170  numedglnl  29179  umgredgnlp  29182  edgusgr  29195  usgruspgrb  29218  uhgr2edg  29243  usgredg2v  29262  ushgredgedgloop  29266  usgr1e  29280  usgrexmplef  29294  subumgredg2  29320  umgrreslem  29340  cusgrexilem2  29477  cusgrexg  29479  fusgrn0degnn0  29535  umgr2v2e  29561  vdiscusgr  29567  rusgr1vtxlem  29623  rgrusgrprc  29625  wlkon2n0  29702  upgrwlkdvdelem  29772  spthonepeq  29788  usgr2wlkneq  29792  iswwlksn  29871  wwlksnon  29884  wwlksn0  29896  wlkiswwlksupgr2  29910  wlknwwlksnbij  29921  wwlksnextbi  29927  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextbij  29935  2pthon3v  29976  umgr2wlk  29982  rusgrnumwwlkb0  30004  isclwwlkn  30059  clwwlkn1loopb  30075  hashecclwwlkn1  30109  s2elclwwlknon2  30136  uhgr3cyclex  30214  frgrwopreglem4a  30342  frgrwopreglem3  30346  frgrwopreglem5lem  30352  frgrwopreglem5  30353  frgrregorufr0  30356  friendshipgt3  30430  nvz  30701  nmlno0i  30826  norm1exi  31282  pjoc1  31466  pjoc2  31471  pj11  31746  elnlfn  31960  nmlnop0  32030  adjbd1o  32117  strlem1  32282  stcltr1i  32306  2ndimaxp  32665  fnpreimac  32689  isarchi  33162  ply1dg1rt  33569  minplyval  33698  qtophaus  33782  locfinreflem  33786  rhmpreimacn  33831  isrrext  33946  indf1ofs  33990  eulerpartlemsv3  34326  eulerpartlemgvv  34341  ballotlemelo  34452  ballotlemfmpn  34459  ballotlemiex  34466  ballotlemi1  34467  ballotlemii  34468  ballotlemfrcn0  34494  ballotlemirc  34496  bnj229  34860  bnj517  34861  bnj590  34886  bnj1097  34957  bnj1118  34960  bnj1128  34966  bnj1145  34969  f1resfz0f1d  35081  loop1cycl  35105  umgr2cycl  35109  subfacp1lem3  35150  cvmlift3lem5  35291  satffunlem1lem1  35370  satffunlem2lem1  35372  satffunlem2lem2  35374  mthmi  35545  rankeq1o  36135  weiunfr  36433  finxpreclem6  37362  poimirlem13  37593  poimirlem14  37594  poimirlem17  37597  poimirlem18  37598  poimirlem21  37601  poimirlem27  37607  poimirlem28  37608  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  lfl1  39026  lshpkrex  39074  cdleme50rnlem  40501  dochkr1  41435  dochkr1OLDN  41436  lcfrlem28  41527  mapd1o  41605  hdmap1vallem  41754  aks6d1c4  42081  hashnexinjle  42086  sticksstones2  42104  sticksstones3  42105  aks6d1c6lem3  42129  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  grpods  42151  unitscyglem1  42152  unitscyglem2  42153  unitscyglem3  42154  unitscyglem4  42155  unitscyglem5  42156  diophrw  42715  eldioph3  42722  diophin  42728  eq0rabdioph  42732  eldioph4b  42767  fphpdo  42773  fnwe2lem2  43008  fnwe2lem3  43009  islssfgi  43029  hbt  43087  dgraaval  43101  dgraalem  43102  dgraaub  43105  mpaaeu  43107  mpaaval  43108  mpaalem  43109  rngunsnply  43130  idomsubgmo  43154  proot1mul  43155  cantnfresb  43286  fvelrnbf  44918  wessf1ornlem  45092  sumnnodd  45551  fourierdlem2  46030  fourierdlem3  46031  fcoresf1  46984  uniimafveqt  47255  elsetpreimafvrab  47268  prpair  47375  prproropf1olem1  47377  pairreueq  47384  paireqne  47385  prprspr2  47392  reuprpr  47397  requad2  47497  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785  clnbgrgrim  47786  usgrgrtrirex  47799  uspgrlimlem1  47812  uspgrlimlem2  47813  grlimgrtri  47820  usgrexmpl1lem  47836  usgrexmpl2lem  47841  uspgrsprfo  47871  ply1mulgsumlem2  48116  lindslinindsimp1  48186  snlindsntor  48200  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  nn0sumshdig  48357