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

Theorem fveqeq2 6384
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 6383 1 (𝐴 = 𝐵 → ((𝐹𝐴) = 𝐶 ↔ (𝐹𝐵) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  cfv 6068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076
This theorem is referenced by:  dff13f  6705  f1veqaeq  6706  f1elima  6712  fpropnf1  6716  oteqimp  7385  suppfnss  7522  suppssfv  7534  tz7.48lem  7740  seqomlem1  7749  seqomlem2  7750  fofinf1o  8448  fipreima  8479  cantnfp1lem3  8792  tcrank  8962  updjudhcoinlf  9009  updjudhcoinrg  9010  pm54.43lem  9076  ackbij1lem18  9312  ackbij1  9313  axcc2  9512  iunfo  9614  grur1  9895  injresinjlem  12796  injresinj  12797  suppssfz  13001  seqid2  13054  hashrabsn01  13364  hashrabsn1  13365  hashimarni  13429  hashbclem  13437  hashbc  13438  hash2exprb  13454  elss2prb  13470  hash2sspr  13471  fi1uzind  13480  wrdmap  13517  wrdl1s1  13585  wrdind  13720  wrdindOLD  13721  wrd2ind  13722  wrd2indOLD  13723  reuccats1lemOLD  13725  reuccats1OLD  13726  reuccatpfxs1  13761  cshf1  13839  cshw1  13851  wwlktovf  13986  wwlktovf1  13987  wwlktovfo  13988  wrd2f1tovbij  13990  wrdl3s3  13992  abs1m  14360  sumrblem  14727  fsumcvg  14728  summolem2a  14731  incexc2  14854  ntrivcvgfvn0  14914  prodrblem  14942  fprodcvg  14943  prodmolem2a  14947  smupvallem  15486  smu01lem  15488  algfx  15574  iserodd  15819  prmreclem2  15900  prmreclem3  15901  vdwlem2  15965  vdwlem6  15969  vdwlem8  15971  hashbcval  15985  ramub1lem1  16009  ramub1lem2  16010  imasleval  16467  eldmcoa  16980  coaval  16983  ghmf1  17953  orbsta  18009  symgextf1  18104  psgnunilem2  18179  psgnunilem3  18180  psgnunilem4  18181  odeq1  18241  odngen  18256  sylow1lem2  18278  sylow1lem4  18280  sylow1lem5  18281  pgpfi  18284  efgtlen  18403  efgsfo  18417  efgredlemd  18422  efgred  18427  gsummptnn0fzfv  18651  isabvd  19089  abveq0  19095  abvdom  19107  islbs  19348  cply1mul  19937  isobs  20340  mdetunilem1  20695  mdetunilem4  20698  mdetunilem8  20702  mdetunilem9  20703  pmatcoe1fsupp  20785  m2cpminvid2lem  20838  mp2pm2mplem4  20893  2ndci  21531  2ndcsb  21532  2ndcsep  21542  txkgen  21735  nmoeq0  22819  nmoleub3  23197  ivth  23512  ivthle  23514  ivthle2  23515  ovolunlem1  23555  ovolicc2  23580  volivth  23665  mbfinf  23723  itg2splitlem  23806  rollelem  24043  rolle  24044  tdeglem4  24111  mdeglt  24116  deg1leb  24146  deg1lt  24148  fta1g  24218  ig1peu  24222  ig1pval3  24225  dgrle  24290  0dgrb  24293  dgreq0  24312  fta1lem  24353  fta1  24354  aannenlem1  24374  aannenlem2  24375  aalioulem2  24379  reeff1o  24492  eflogeq  24639  argregt0  24647  argrege0  24648  efopn  24695  asinsinb  24915  acoscosb  24916  atantanb  24942  musum  25208  dchrptlem1  25280  dchrptlem2  25281  lgsquadlem1  25396  istrkgl  25648  mirreu  25850  israg  25883  lmireu  25973  lmieq  25974  gropd  26200  grstructd  26201  umgredg2  26272  umgrbi  26273  umgrnloopv  26278  umgredgprv  26279  edgumgr  26307  numedglnl  26317  umgredgnlp  26320  edgusgr  26333  usgruspgrb  26354  uhgr2edg  26378  usgredg2v  26397  ushgredgedgloop  26401  usgr1e  26416  usgrexmplef  26430  subumgredg2  26456  umgrreslem  26476  cusgrexilem2  26629  cusgrexg  26631  fusgrn0degnn0  26686  umgr2v2e  26712  vdiscusgr  26718  rusgr1vtxlem  26774  rgrusgrprc  26776  wlkon2n0  26853  wlkres  26859  upgrwlkdvdelem  26924  spthonepeq  26940  usgr2wlkneq  26944  iswwlksn  27023  wwlksnon  27037  wwlksn0  27054  wlkiswwlksupgr2  27068  wlknwwlksnbij  27084  wwlksnextbi  27097  wwlksnextbiOLD  27098  wwlksnextfun  27104  wwlksnextinj  27105  wwlksnextfunOLD  27109  wwlksnextinjOLD  27110  wwlksnextbij  27113  wwlksnextbijOLD  27114  2pthon3v  27166  umgr2wlk  27172  rusgrnumwwlkb0  27196  isclwwlkn  27266  clwwlkn1loopb  27286  hashecclwwlkn1  27329  s2elclwwlknon2  27377  uhgr3cyclex  27460  frgrwopreglem4a  27590  frgrwopreglem3  27594  frgrwopreglem5lem  27600  frgrwopreglem5  27601  frgrregorufr0  27604  friendshipgt3  27714  nvz  27980  nmlno0i  28105  norm1exi  28563  pjoc1  28749  pjoc2  28754  pj11  29029  elnlfn  29243  nmlnop0  29313  adjbd1o  29400  strlem1  29565  stcltr1i  29589  isarchi  30183  fimaproj  30347  qtophaus  30350  locfinreflem  30354  isrrext  30491  indf1ofs  30535  eulerpartlemsv3  30870  eulerpartlemgvv  30885  ballotlemelo  30997  ballotlemfmpn  31004  ballotlemiex  31011  ballotlemi1  31012  ballotlemii  31013  ballotlemfrcn0  31039  ballotlemirc  31041  bnj229  31402  bnj517  31403  bnj590  31428  bnj1097  31497  bnj1118  31500  bnj1128  31506  bnj1145  31509  subfacp1lem3  31612  cvmlift3lem5  31753  mthmi  31922  trpred0  32179  nosupfv  32296  noeta  32312  nocvxmin  32338  scutbday  32357  scutun12  32361  scutbdaylt  32366  rankeq1o  32722  finxpreclem6  33666  poimirlem13  33846  poimirlem14  33847  poimirlem17  33850  poimirlem18  33851  poimirlem21  33854  poimirlem27  33860  poimirlem28  33861  ovoliunnfl  33875  voliunnfl  33877  volsupnfl  33878  lfl1  35026  lshpkrex  35074  cdleme50rnlem  36500  dochkr1  37434  dochkr1OLDN  37435  lcfrlem28  37526  mapd1o  37604  hdmap1vallem  37753  diophrw  38000  eldioph3  38007  diophin  38014  eq0rabdioph  38018  eldioph4b  38053  fphpdo  38059  fnwe2lem2  38298  fnwe2lem3  38299  islssfgi  38319  hbt  38377  dgraaval  38391  dgraalem  38392  dgraaub  38395  mpaaeu  38397  mpaaval  38398  mpaalem  38399  rngunsnply  38420  idomsubgmo  38453  proot1mul  38454  fvelrnbf  39829  wessf1ornlem  40018  fvelimad  40100  sumnnodd  40500  uspgrsprfo  42425  ply1mulgsumlem2  42844  lindslinindsimp1  42915  snlindsntor  42929  nn0sumshdiglemA  43082  nn0sumshdiglemB  43083  nn0sumshdiglem1  43084  nn0sumshdig  43086
  Copyright terms: Public domain W3C validator