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

Theorem fveq1i 6447
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 6445 . 2 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
31, 2ax-mp 5 1 (𝐹𝐴) = (𝐺𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1601  cfv 6135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-rex 3096  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143
This theorem is referenced by:  fveq12i  6452  fvun2  6530  fvopab3ig  6538  fvsnun1  6717  fvsnun1OLD  6719  fvsnun2OLD  6720  fvpr1  6727  fvpr2  6728  fvpr1g  6729  fvpr2g  6730  fvtp1  6732  fvtp2  6733  fvtp3  6734  fvtp1g  6735  fvtp2g  6736  fvtp3g  6737  fpropnf1  6796  fveqf1o  6829  ov  7057  ovigg  7058  ovg  7076  fvresex  7418  curry1  7550  curry2  7553  suppsnop  7590  wfrlem5  7702  tfr2a  7774  rdgsucmptf  7807  rdgsucmptnf  7808  frsucmpt  7816  frsucmptn  7817  seqomlem1  7828  seqomlem3  7830  seqomlem4  7831  seqom0g  7834  seqomsuc  7835  unblem2  8501  inf3lemb  8819  inf3lemc  8820  trcl  8901  r10  8928  r1sucg  8929  r1limg  8931  infxpenc2  9178  aleph0  9222  alephlim  9223  alephsuc  9224  alephfplem1  9260  alephfplem2  9261  ackbij2lem3  9398  cfsmolem  9427  infpssrlem1  9460  infpssrlem2  9461  fin23lem34  9503  fin23lem35  9504  isf32lem6  9515  isf32lem7  9516  isf32lem8  9517  isf34lem5  9535  hsmexlem7  9580  axdclem2  9677  canthp1lem2  9810  wunex2  9895  wuncval2  9904  addpiord  10041  mulpiord  10042  addpqnq  10095  mulpqnq  10098  fseq1p1m1  12732  om2uz0i  13065  om2uzrdg  13074  uzrdg0i  13077  uzrdgsuci  13078  hashkf  13437  hashgval  13438  hashinf  13440  ccat1st1st  13718  revs1  13911  cats1fv  14010  shftidt  14229  cbvsum  14833  fsumss  14863  isumclim3  14895  isumsup2  14982  cbvprod  15048  fprodss  15081  iprodclim3  15133  fprodefsum  15227  ruclem4  15367  ruclem6  15368  ruclem7  15369  sadc0  15582  sadcp1  15583  sadcaddlem  15585  sadaddlem  15594  smup0  15607  smupp1  15608  algr0  15691  algrp1  15693  ndxarg  16280  strfv2d  16301  xpsc0  16606  xpsc1  16607  funcoppc  16920  fthepi  16973  homadm  17075  homacd  17076  prdsidlem  17708  prdsinvlem  17911  cayleylem2  18216  symggen  18273  pmtr3ncomlem1  18276  gsumval3  18694  gsumzaddlem  18707  gsumzmhm  18723  pgpfaclem1  18867  ringidval  18890  lidlval  19589  rspval  19590  lidlnegcl  19611  lpival  19642  eqcoe1ply1eq  20063  evls1val  20081  evl1val  20089  znf1o  20295  mat1dimmul  20687  mdetralt  20819  mdetunilem7  20829  decpmatid  20982  pmatcollpwscmatlem1  21001  cpmidpmat  21085  chcoeffeq  21098  restcls  21393  restntr  21394  upxp  21835  cnmetdval  22982  remetdval  23000  qdensere2  23008  pcoptcl  23228  pcopt  23229  pcopt2  23230  pcorevlem  23233  isncvsngp  23356  cnncvsabsnegdemo  23372  ovolfsval  23674  ovollb2lem  23692  ovolunlem1a  23700  ovoliunlem1  23706  ovoliun2  23710  ovolscalem1  23717  ovolicc2lem4  23724  mblvol  23734  ioombl1lem4  23765  uniioovol  23783  uniioombllem3  23789  0pval  23875  limccnp  24092  limccnp2  24093  dvcnvrelem2  24218  itgsubstlem  24248  ply1remlem  24359  plyrem  24497  qaa  24515  abelth  24632  efif1olem4  24729  eflog  24760  logef  24765  logeftb  24767  dvrelog  24820  dvlog  24834  cxpcn3  24929  efrlim  25148  eflgam  25223  wilthlem3  25248  basellem8  25266  lgsqrlem1  25523  tgcgr4  25882  krippenlem  26041  colperpexlem1  26078  opphllem3  26097  lmiisolem  26144  axlowdimlem8  26298  axlowdimlem9  26299  axlowdimlem11  26301  axlowdimlem12  26302  axlowdimlem17  26307  ushgredgedg  26575  ushgredgedgloop  26577  ushgredgedgloopOLD  26578  subgruhgredgd  26631  vtxdlfgrval  26833  vtxd0nedgb  26836  vtxdushgrfvedg  26838  vtxdginducedm1lem3  26889  finsumvtxdg2size  26898  vtxdgoddnumeven  26901  isrgr  26907  fusgrregdegfi  26917  wlk1walk  26986  wlkres  27019  wlkresOLD  27021  wlkp1lem5  27028  wlkp1lem6  27029  wlkp1lem7  27030  wlkp1lem8  27031  clwlkcompbp  27134  crctcshwlkn0lem4  27162  crctcshwlkn0lem5  27163  crctcshwlkn0lem6  27164  wlkwwlksurOLD  27248  2wlkdlem3  27307  2wlkdlem8  27313  2wlkond  27317  umgr2adedgwlk  27325  1wlkdlem4  27543  1pthond  27547  wlk2v2elem2  27559  3wlkdlem3  27564  3wlkdlem8  27570  3cycld  27581  3cyclpd  27582  eucrctshift  27647  frgrncvvdeq  27717  frgrwopreglem2  27721  avril1  27894  vafval  28030  smfval  28032  0vfval  28033  nmcvfval  28034  vsfval  28060  hhssabloilem  28690  pjoc2i  28869  pjcji  29115  ho0val  29181  hoival  29186  adjbdlnb  29515  nmopcoadji  29532  opsqrlem2  29572  opsqrlem5  29575  hmopidmchi  29582  hmopidmpji  29583  pjinvari  29622  pjadj2coi  29635  pj3lem1  29637  funcnvmpt  30032  pmtrprfv2  30446  madjusmdetlem1  30491  cnre2csqlem  30554  zzsnm  30603  rrhcn  30639  qqhre  30662  oms0  30957  omsmon  30958  omssubaddlem  30959  omssubadd  30960  eulerpart  31042  fib0  31060  fib1  31061  fibp1  31062  coinflippv  31144  gsumnunsn  31214  derangenlem  31752  kur14lem2  31788  kur14lem3  31789  kur14lem5  31791  kur14lem6  31792  txsconnlem  31821  cvmliftlem4  31869  cvmliftlem5  31870  trpredmintr  32319  trpred0  32324  frrlem5  32373  noetalem3  32454  funpartfv  32641  fullfunfv  32643  neibastop2lem  32943  dffinxpf  33817  ftc1cnnc  34109  heiborlem4  34237  heiborlem6  34239  cdlemk13  37006  cdlemk14  37008  cdlemk15  37009  cdlemk21N  37027  cdlemk20  37028  cdlemk56w  37127  lcfrlem1  37696  hdmapfval  37981  rabdiophlem2  38326  dnnumch1  38573  aomclem6  38588  mncn0  38668  aaitgo  38691  rngunsnply  38702  cytpval  38746  dssmapntrcls  39382  binomcxplemdvsum  39510  binomcxplemnotnn0  39511  binomcxp  39512  fvcod  40342  fsumsermpt  40719  fmul01  40720  fmuldfeq  40723  fmul01lt1lem1  40724  fmul01lt1lem2  40725  lptioo2cn  40785  lptioo1cn  40786  limclner  40791  dvsinax  41055  fperdvper  41061  dvnmul  41086  dvnprodlem1  41089  dvnprodlem2  41090  dvnprodlem3  41091  itgsin0pilem1  41093  stoweidlem3  41147  stoweidlem17  41161  stoweidlem47  41191  fourierdlem42  41293  fourierdlem62  41312  fourierdlem80  41330  fourierdlem90  41340  fourierdlem92  41342  fourierdlem93  41343  fourierdlem103  41353  fourierdlem104  41354  fouriercnp  41370  sge0isum  41568  sge0seq  41587  ovnsubadd  41713  vonn0ioo  41828  vonn0icc  41829  smflimsup  41961  isomushgr  42739  rhmsubclem2  43102  rhmsubcALTVlem2  43120  ply1mulgsum  43193  lineval  43197  lincvalpr  43222  lindslinindimp2lem4  43265  zlmodzxzldeplem3  43306  zlmodzxzldeplem4  43307  ehl2eudisval0  43461  2sphere0  43486  line2  43488  line2x  43490  line2y  43491  itscnhlinecirc02p  43521
  Copyright terms: Public domain W3C validator