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

Theorem fveq1i 6089
Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
fveq1i.1 𝐹 = 𝐺
Assertion
Ref Expression
fveq1i (𝐹𝐴) = (𝐺𝐴)

Proof of Theorem fveq1i
StepHypRef Expression
1 fveq1i.1 . 2 𝐹 = 𝐺
2 fveq1 6087 . 2 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
31, 2ax-mp 5 1 (𝐹𝐴) = (𝐺𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798
This theorem is referenced by:  fveq12i  6093  fvun2  6165  fvopab3ig  6173  fvsnun1  6331  fvsnun2  6332  fvpr1  6339  fvpr2  6340  fvpr1g  6341  fvpr2g  6342  fvtp1  6343  fvtp2  6344  fvtp3  6345  fvtp1g  6346  fvtp2g  6347  fvtp3g  6348  fveqf1o  6435  ov  6656  ovigg  6657  ovg  6675  fvresex  7009  curry1  7133  curry2  7136  suppsnop  7173  wfrlem5  7283  tfr2a  7355  rdgsucmptf  7388  rdgsucmptnf  7389  frsucmpt  7397  frsucmptn  7398  seqomlem1  7409  seqomlem3  7411  seqomlem4  7412  seqom0g  7415  seqomsuc  7416  unblem2  8075  inf3lemb  8382  inf3lemc  8383  trcl  8464  r10  8491  r1sucg  8492  r1limg  8494  infxpenc2  8705  aleph0  8749  alephlim  8750  alephsuc  8751  alephfplem1  8787  alephfplem2  8788  ackbij2lem3  8923  cfsmolem  8952  infpssrlem1  8985  infpssrlem2  8986  fin23lem34  9028  fin23lem35  9029  isf32lem6  9040  isf32lem7  9041  isf32lem8  9042  isf34lem5  9060  hsmexlem7  9105  axdclem2  9202  canthp1lem2  9331  wunex2  9416  wuncval2  9425  addpiord  9562  mulpiord  9563  addpqnq  9616  mulpqnq  9619  fseq1p1m1  12238  om2uz0i  12563  om2uzrdg  12572  uzrdg0i  12575  uzrdgsuci  12576  hashkf  12936  hashgval  12937  hashinf  12939  revs1  13311  cats1fv  13401  shftidt  13616  cbvsum  14219  fsumss  14249  isumclim3  14278  isumsup2  14363  cbvprod  14430  fprodss  14463  iprodclim3  14516  fprodefsum  14610  ruclem4  14748  ruclem6  14749  ruclem7  14750  sadc0  14960  sadcp1  14961  sadcaddlem  14963  sadaddlem  14972  smup0  14985  smupp1  14986  algr0  15069  algrp1  15071  ndxarg  15661  strfv2d  15679  xpsc0  15989  xpsc1  15990  funcoppc  16304  fthepi  16357  homadm  16459  homacd  16460  prdsidlem  17091  prdsinvlem  17293  cayleylem2  17602  symggen  17659  pmtr3ncomlem1  17662  gsumval3  18077  gsumzaddlem  18090  gsumzmhm  18106  pgpfaclem1  18249  ringidval  18272  lidlval  18959  rspval  18960  lidlnegcl  18981  lpival  19012  eqcoe1ply1eq  19434  evls1val  19452  evl1val  19460  znf1o  19664  mat1dimmul  20043  mdetralt  20175  mdetunilem7  20185  decpmatid  20336  pmatcollpwscmatlem1  20355  cpmidpmat  20439  chcoeffeq  20452  restcls  20737  restntr  20738  upxp  21178  cnmetdval  22316  remetdval  22332  qdensere2  22340  pcoptcl  22560  pcopt  22561  pcopt2  22562  pcorevlem  22565  isncvsngp  22683  cnncvsabsnegdemo  22697  ovolfsval  22963  ovollb2lem  22980  ovolunlem1a  22988  ovoliunlem1  22994  ovoliun2  22998  ovolscalem1  23005  ovolicc2lem4  23012  mblvol  23022  ioombl1lem4  23053  uniioovol  23070  uniioombllem3  23076  0pval  23161  limccnp  23378  limccnp2  23379  dvcnvrelem2  23502  itgsubstlem  23532  ply1remlem  23643  plyrem  23781  qaa  23799  abelth  23916  efif1olem4  24012  eflog  24044  logef  24049  logeftb  24051  dvrelog  24100  dvlog  24114  cxpcn3  24206  efrlim  24413  eflgam  24488  wilthlem3  24513  basellem8  24531  lgsqrlem1  24788  tgcgr4  25144  krippenlem  25303  colperpexlem1  25340  opphllem3  25359  lmiisolem  25406  axlowdimlem8  25547  axlowdimlem9  25548  axlowdimlem11  25550  axlowdimlem12  25551  axlowdimlem17  25556  2wlklemA  25850  2wlklemB  25851  2wlklemC  25852  wlkntrllem2  25856  wlkntrllem3  25857  constr3lem4  25941  constr3lem5  25942  wlkiswwlksur  26013  vdgr1c  26198  eupares  26268  eupap1  26269  vdegp1ai  26277  vdegp1bi  26278  avril1  26477  vafval  26626  smfval  26628  0vfval  26629  nmcvfval  26630  vsfval  26658  hhssabloilem  27308  pjoc2i  27487  pjcji  27733  ho0val  27799  hoival  27804  adjbdlnb  28133  nmopcoadji  28150  opsqrlem2  28190  opsqrlem5  28193  hmopidmchi  28200  hmopidmpji  28201  pjinvari  28240  pjadj2coi  28253  pj3lem1  28255  funcnvmptOLD  28656  funcnvmpt  28657  pmtrprfv2  28985  madjusmdetlem1  29027  cnre2csqlem  29090  zzsnm  29139  rrhcn  29175  qqhre  29198  oms0  29492  omsmon  29493  omssubaddlem  29494  omssubadd  29495  eulerpart  29577  fib0  29594  fib1  29595  fibp1  29596  coinflippv  29678  gsumnunsn  29748  derangenlem  30213  kur14lem2  30249  kur14lem3  30250  kur14lem5  30252  kur14lem6  30253  txsconlem  30282  cvmliftlem4  30330  cvmliftlem5  30331  trpredmintr  30781  trpred0  30786  frrlem5  30834  funpartfv  31028  fullfunfv  31030  neibastop2lem  31331  dffinxpf  32194  ftc1cnnc  32450  heiborlem4  32579  heiborlem6  32581  cdlemk13  34954  cdlemk14  34956  cdlemk15  34957  cdlemk21N  34975  cdlemk20  34976  cdlemk56w  35075  lcfrlem1  35645  hdmapfval  35933  rabdiophlem2  36180  dnnumch1  36428  aomclem6  36443  mncn0  36524  aaitgo  36547  rngunsnply  36558  cytpval  36602  dssmapntrcls  37242  binomcxplemdvsum  37372  binomcxplemnotnn0  37373  binomcxp  37374  fvcod  38214  fsumsermpt  38443  fmul01  38444  fmuldfeq  38447  fmul01lt1lem1  38448  fmul01lt1lem2  38449  lptioo2cn  38509  lptioo1cn  38510  limclner  38515  dvsinax  38598  fperdvper  38605  dvnmul  38630  dvnprodlem1  38633  dvnprodlem2  38634  dvnprodlem3  38635  itgsin0pilem1  38638  stoweidlem3  38693  stoweidlem17  38707  stoweidlem47  38737  fourierdlem42  38839  fourierdlem62  38858  fourierdlem80  38876  fourierdlem90  38886  fourierdlem92  38888  fourierdlem93  38889  fourierdlem103  38899  fourierdlem104  38900  fouriercnp  38916  sge0isum  39117  sge0seq  39136  ovnsubadd  39259  vonn0ioo  39375  vonn0icc  39376  fpropnf1  40157  ushgredgedga  40451  ushgredgedgaloop  40453  subgruhgredgd  40503  vtxdlfgrval  40695  vtxd0nedgb  40698  vtxdushgrfvedg  40700  isrgr  40754  fusgrregdegfi  40764  1wlk1walk  40838  1wlkres  40874  1wlkp1lem5  40881  1wlkp1lem6  40882  1wlkp1lem7  40883  1wlkp1lem8  40884  crctcsh1wlkn0lem4  41011  crctcsh1wlkn0lem5  41012  crctcsh1wlkn0lem6  41013  wlkwwlksur  41089  21wlkdlem3  41129  21wlkdlem8  41135  21wlkond  41139  umgr2adedgwlk  41147  11wlkdlem4  41302  1pthond  41306  1wlk2v2elem2  41318  31wlkdlem3  41323  31wlkdlem8  41329  3cycld  41340  3cyclpd  41341  eucrctshift  41406  frgrncvvdeq  41475  frgrwopreglem2  41477  rhmsubclem2  41874  rhmsubcALTVlem2  41893  ply1mulgsum  41967  lineval  41971  lincvalpr  41996  lindslinindimp2lem4  42039  zlmodzxzldeplem3  42080  zlmodzxzldeplem4  42081
  Copyright terms: Public domain W3C validator