MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fveqeq2 Structured version   Visualization version   GIF version

Theorem fveqeq2 6682
Description: Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)
Assertion
Ref Expression
fveqeq2 (𝐴 = 𝐵 → ((𝐹𝐴) = 𝐶 ↔ (𝐹𝐵) = 𝐶))

Proof of Theorem fveqeq2
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21fveqeq2d 6681 1 (𝐴 = 𝐵 → ((𝐹𝐴) = 𝐶 ↔ (𝐹𝐵) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1536  cfv 6358
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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366
This theorem is referenced by:  fvelimad  6735  dff13f  7017  f1veqaeq  7018  f1elima  7024  fpropnf1  7028  nf1const  7062  oteqimp  7711  fimaproj  7832  suppfnss  7858  suppssfv  7869  tz7.48lem  8080  seqomlem1  8089  seqomlem2  8090  fofinf1o  8802  fipreima  8833  cantnfp1lem3  9146  tcrank  9316  updjudhcoinlf  9364  updjudhcoinrg  9365  pm54.43lem  9431  ackbij1lem18  9662  ackbij1  9663  axcc2  9862  iunfo  9964  grur1  10245  injresinjlem  13160  injresinj  13161  suppssfz  13365  seqid2  13419  hashrabsn01  13737  hashrabsn1  13738  hashimarni  13805  hashbclem  13813  hashbc  13814  hash2exprb  13832  elss2prb  13848  hash2sspr  13849  fi1uzind  13858  wrdmap  13900  wrdl1s1  13971  wrdind  14087  wrd2ind  14088  reuccatpfxs1lem  14111  reuccatpfxs1  14112  cshf1  14175  cshw1  14187  wwlktovf  14323  wwlktovf1  14324  wwlktovfo  14325  wrd2f1tovbij  14327  wrdl3s3  14329  abs1m  14698  sumrblem  15071  fsumcvg  15072  summolem2a  15075  incexc2  15196  ntrivcvgfvn0  15258  prodrblem  15286  fprodcvg  15287  prodmolem2a  15291  smupvallem  15835  smu01lem  15837  algfx  15927  iserodd  16175  prmreclem2  16256  prmreclem3  16257  vdwlem2  16321  vdwlem6  16325  vdwlem8  16327  hashbcval  16341  ramub1lem1  16365  ramub1lem2  16366  imasleval  16817  eldmcoa  17328  coaval  17331  ghmf1  18390  orbsta  18446  symgextf1  18552  psgnunilem2  18626  psgnunilem3  18627  psgnunilem4  18628  odeq1  18690  odngen  18705  sylow1lem2  18727  sylow1lem4  18729  sylow1lem5  18730  pgpfi  18733  efgtlen  18855  efgsfo  18868  efgredlemd  18873  efgred  18877  gsummptnn0fzfv  19110  isabvd  19594  abveq0  19600  abvdom  19612  islbs  19851  cply1mul  20465  isobs  20867  mdetunilem1  21224  mdetunilem4  21227  mdetunilem8  21231  mdetunilem9  21232  pmatcoe1fsupp  21312  m2cpminvid2lem  21365  mp2pm2mplem4  21420  2ndci  22059  2ndcsb  22060  2ndcsep  22070  txkgen  22263  nmoeq0  23348  nmoleub3  23726  ivth  24058  ivthle  24060  ivthle2  24061  ovolunlem1  24101  ovolicc2  24126  volivth  24211  mbfinf  24269  itg2splitlem  24352  rollelem  24589  rolle  24590  tdeglem4  24657  mdeglt  24662  deg1leb  24692  deg1lt  24694  fta1g  24764  ig1peu  24768  ig1pval3  24771  dgrle  24836  0dgrb  24839  dgreq0  24858  fta1lem  24899  fta1  24900  aannenlem1  24920  aannenlem2  24921  aalioulem2  24925  reeff1o  25038  eflogeq  25188  argregt0  25196  argrege0  25197  efopn  25244  asinsinb  25478  acoscosb  25479  atantanb  25505  musum  25771  dchrptlem1  25843  dchrptlem2  25844  lgsquadlem1  25959  istrkgl  26247  mirreu  26453  israg  26486  lmireu  26579  lmieq  26580  gropd  26819  grstructd  26820  umgredg2  26888  umgrbi  26889  umgrnloopv  26894  umgredgprv  26895  edgumgr  26923  numedglnl  26932  umgredgnlp  26935  edgusgr  26948  usgruspgrb  26969  uhgr2edg  26993  usgredg2v  27012  ushgredgedgloop  27016  usgr1e  27030  usgrexmplef  27044  subumgredg2  27070  umgrreslem  27090  cusgrexilem2  27227  cusgrexg  27229  fusgrn0degnn0  27284  umgr2v2e  27310  vdiscusgr  27316  rusgr1vtxlem  27372  rgrusgrprc  27374  wlkon2n0  27451  upgrwlkdvdelem  27520  spthonepeq  27536  usgr2wlkneq  27540  iswwlksn  27619  wwlksnon  27632  wwlksn0  27644  wlkiswwlksupgr2  27658  wlknwwlksnbij  27669  wwlksnextbi  27675  wwlksnextfun  27679  wwlksnextinj  27680  wwlksnextbij  27683  2pthon3v  27725  umgr2wlk  27731  rusgrnumwwlkb0  27753  isclwwlkn  27808  clwwlkn1loopb  27824  hashecclwwlkn1  27859  s2elclwwlknon2  27886  uhgr3cyclex  27964  frgrwopreglem4a  28092  frgrwopreglem3  28096  frgrwopreglem5lem  28102  frgrwopreglem5  28103  frgrregorufr0  28106  friendshipgt3  28180  nvz  28449  nmlno0i  28574  norm1exi  29030  pjoc1  29214  pjoc2  29219  pj11  29494  elnlfn  29708  nmlnop0  29778  adjbd1o  29865  strlem1  30030  stcltr1i  30054  fnpreimac  30419  isarchi  30815  qtophaus  31104  locfinreflem  31108  isrrext  31245  indf1ofs  31289  eulerpartlemsv3  31623  eulerpartlemgvv  31638  ballotlemelo  31749  ballotlemfmpn  31756  ballotlemiex  31763  ballotlemi1  31764  ballotlemii  31765  ballotlemfrcn0  31791  ballotlemirc  31793  bnj229  32160  bnj517  32161  bnj590  32186  bnj1097  32257  bnj1118  32260  bnj1128  32266  bnj1145  32269  f1resfz0f1d  32365  loop1cycl  32388  umgr2cycl  32392  subfacp1lem3  32433  cvmlift3lem5  32574  satffunlem1lem1  32653  satffunlem2lem1  32655  satffunlem2lem2  32657  mthmi  32828  trpred0  33079  nosupfv  33210  noeta  33226  nocvxmin  33252  scutbday  33271  scutun12  33275  scutbdaylt  33280  rankeq1o  33636  finxpreclem6  34681  poimirlem13  34909  poimirlem14  34910  poimirlem17  34913  poimirlem18  34914  poimirlem21  34917  poimirlem27  34923  poimirlem28  34924  ovoliunnfl  34938  voliunnfl  34940  volsupnfl  34941  lfl1  36210  lshpkrex  36258  cdleme50rnlem  37684  dochkr1  38618  dochkr1OLDN  38619  lcfrlem28  38710  mapd1o  38788  hdmap1vallem  38937  diophrw  39362  eldioph3  39369  diophin  39375  eq0rabdioph  39379  eldioph4b  39414  fphpdo  39420  fnwe2lem2  39657  fnwe2lem3  39658  islssfgi  39678  hbt  39736  dgraaval  39750  dgraalem  39751  dgraaub  39754  mpaaeu  39756  mpaaval  39757  mpaalem  39758  rngunsnply  39779  idomsubgmo  39804  proot1mul  39805  fvelrnbf  41281  wessf1ornlem  41451  sumnnodd  41917  fourierdlem2  42401  fourierdlem3  42402  uniimafveqt  43548  elsetpreimafvrab  43561  prpair  43670  prproropf1olem1  43672  pairreueq  43679  paireqne  43680  prprspr2  43687  reuprpr  43692  requad2  43795  uspgrsprfo  44030  ply1mulgsumlem2  44448  lindslinindsimp1  44519  snlindsntor  44533  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  nn0sumshdiglem1  44688  nn0sumshdig  44690
  Copyright terms: Public domain W3C validator