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

Theorem fveq1i 6230
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 6228 . 2 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
31, 2ax-mp 5 1 (𝐹𝐴) = (𝐺𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934
This theorem is referenced by:  fveq12i  6234  fvun2  6309  fvopab3ig  6317  fvsnun1  6489  fvsnun2  6490  fvpr1  6497  fvpr2  6498  fvpr1g  6499  fvpr2g  6500  fvtp1  6501  fvtp2  6502  fvtp3  6503  fvtp1g  6504  fvtp2g  6505  fvtp3g  6506  fpropnf1  6564  fveqf1o  6597  ov  6822  ovigg  6823  ovg  6841  fvresex  7181  curry1  7314  curry2  7317  suppsnop  7354  wfrlem5  7464  tfr2a  7536  rdgsucmptf  7569  rdgsucmptnf  7570  frsucmpt  7578  frsucmptn  7579  seqomlem1  7590  seqomlem3  7592  seqomlem4  7593  seqom0g  7596  seqomsuc  7597  unblem2  8254  inf3lemb  8560  inf3lemc  8561  trcl  8642  r10  8669  r1sucg  8670  r1limg  8672  infxpenc2  8883  aleph0  8927  alephlim  8928  alephsuc  8929  alephfplem1  8965  alephfplem2  8966  ackbij2lem3  9101  cfsmolem  9130  infpssrlem1  9163  infpssrlem2  9164  fin23lem34  9206  fin23lem35  9207  isf32lem6  9218  isf32lem7  9219  isf32lem8  9220  isf34lem5  9238  hsmexlem7  9283  axdclem2  9380  canthp1lem2  9513  wunex2  9598  wuncval2  9607  addpiord  9744  mulpiord  9745  addpqnq  9798  mulpqnq  9801  fseq1p1m1  12452  om2uz0i  12786  om2uzrdg  12795  uzrdg0i  12798  uzrdgsuci  12799  hashkf  13159  hashgval  13160  hashinf  13162  ccat1st1st  13448  revs1  13560  cats1fv  13650  shftidt  13866  cbvsum  14469  fsumss  14500  isumclim3  14534  isumsup2  14622  cbvprod  14689  fprodss  14722  iprodclim3  14775  fprodefsum  14869  ruclem4  15007  ruclem6  15008  ruclem7  15009  sadc0  15223  sadcp1  15224  sadcaddlem  15226  sadaddlem  15235  smup0  15248  smupp1  15249  algr0  15332  algrp1  15334  ndxarg  15929  strfv2d  15952  xpsc0  16267  xpsc1  16268  funcoppc  16582  fthepi  16635  homadm  16737  homacd  16738  prdsidlem  17369  prdsinvlem  17571  cayleylem2  17879  symggen  17936  pmtr3ncomlem1  17939  gsumval3  18354  gsumzaddlem  18367  gsumzmhm  18383  pgpfaclem1  18526  ringidval  18549  lidlval  19240  rspval  19241  lidlnegcl  19262  lpival  19293  eqcoe1ply1eq  19715  evls1val  19733  evl1val  19741  znf1o  19948  mat1dimmul  20330  mdetralt  20462  mdetunilem7  20472  decpmatid  20623  pmatcollpwscmatlem1  20642  cpmidpmat  20726  chcoeffeq  20739  restcls  21033  restntr  21034  upxp  21474  cnmetdval  22621  remetdval  22639  qdensere2  22647  pcoptcl  22867  pcopt  22868  pcopt2  22869  pcorevlem  22872  isncvsngp  22995  cnncvsabsnegdemo  23011  ovolfsval  23285  ovollb2lem  23302  ovolunlem1a  23310  ovoliunlem1  23316  ovoliun2  23320  ovolscalem1  23327  ovolicc2lem4  23334  mblvol  23344  ioombl1lem4  23375  uniioovol  23393  uniioombllem3  23399  0pval  23483  limccnp  23700  limccnp2  23701  dvcnvrelem2  23826  itgsubstlem  23856  ply1remlem  23967  plyrem  24105  qaa  24123  abelth  24240  efif1olem4  24336  eflog  24368  logef  24373  logeftb  24375  dvrelog  24428  dvlog  24442  cxpcn3  24534  efrlim  24741  eflgam  24816  wilthlem3  24841  basellem8  24859  lgsqrlem1  25116  tgcgr4  25471  krippenlem  25630  colperpexlem1  25667  opphllem3  25686  lmiisolem  25733  axlowdimlem8  25874  axlowdimlem9  25875  axlowdimlem11  25877  axlowdimlem12  25878  axlowdimlem17  25883  ushgredgedg  26166  ushgredgedgloop  26168  subgruhgredgd  26221  vtxdlfgrval  26437  vtxd0nedgb  26440  vtxdushgrfvedg  26442  vtxdginducedm1lem3  26493  finsumvtxdg2size  26502  vtxdgoddnumeven  26505  isrgr  26511  fusgrregdegfi  26521  wlk1walk  26591  wlkres  26623  wlkp1lem5  26630  wlkp1lem6  26631  wlkp1lem7  26632  wlkp1lem8  26633  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem6  26763  wlkwwlksur  26851  2wlkdlem3  26892  2wlkdlem8  26898  2wlkond  26902  umgr2adedgwlk  26910  1wlkdlem4  27118  1pthond  27122  wlk2v2elem2  27134  3wlkdlem3  27139  3wlkdlem8  27145  3cycld  27156  3cyclpd  27157  eucrctshift  27221  frgrncvvdeq  27289  frgrwopreglem2  27293  avril1  27449  vafval  27586  smfval  27588  0vfval  27589  nmcvfval  27590  vsfval  27616  hhssabloilem  28246  pjoc2i  28425  pjcji  28671  ho0val  28737  hoival  28742  adjbdlnb  29071  nmopcoadji  29088  opsqrlem2  29128  opsqrlem5  29131  hmopidmchi  29138  hmopidmpji  29139  pjinvari  29178  pjadj2coi  29191  pj3lem1  29193  funcnvmptOLD  29595  funcnvmpt  29596  pmtrprfv2  29976  madjusmdetlem1  30021  cnre2csqlem  30084  zzsnm  30133  rrhcn  30169  qqhre  30192  oms0  30487  omsmon  30488  omssubaddlem  30489  omssubadd  30490  eulerpart  30572  fib0  30589  fib1  30590  fibp1  30591  coinflippv  30673  gsumnunsn  30743  derangenlem  31279  kur14lem2  31315  kur14lem3  31316  kur14lem5  31318  kur14lem6  31319  txsconnlem  31348  cvmliftlem4  31396  cvmliftlem5  31397  trpredmintr  31855  trpred0  31860  frrlem5  31909  noetalem3  31990  funpartfv  32177  fullfunfv  32179  neibastop2lem  32480  dffinxpf  33352  ftc1cnnc  33614  heiborlem4  33743  heiborlem6  33745  cdlemk13  36457  cdlemk14  36459  cdlemk15  36460  cdlemk21N  36478  cdlemk20  36479  cdlemk56w  36578  lcfrlem1  37148  hdmapfval  37436  rabdiophlem2  37683  dnnumch1  37931  aomclem6  37946  mncn0  38026  aaitgo  38049  rngunsnply  38060  cytpval  38104  dssmapntrcls  38743  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  binomcxp  38873  fvcod  39737  fsumsermpt  40129  fmul01  40130  fmuldfeq  40133  fmul01lt1lem1  40134  fmul01lt1lem2  40135  lptioo2cn  40195  lptioo1cn  40196  limclner  40201  dvsinax  40445  fperdvper  40451  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  itgsin0pilem1  40483  stoweidlem3  40538  stoweidlem17  40552  stoweidlem47  40582  fourierdlem42  40684  fourierdlem62  40703  fourierdlem80  40721  fourierdlem90  40731  fourierdlem92  40733  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  fouriercnp  40761  sge0isum  40962  sge0seq  40981  ovnsubadd  41107  vonn0ioo  41222  vonn0icc  41223  smflimsup  41355  rhmsubclem2  42412  rhmsubcALTVlem2  42430  ply1mulgsum  42503  lineval  42507  lincvalpr  42532  lindslinindimp2lem4  42575  zlmodzxzldeplem3  42616  zlmodzxzldeplem4  42617
  Copyright terms: Public domain W3C validator