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

Theorem fveq1i 6662
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 6660 . 2 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
31, 2ax-mp 5 1 (𝐹𝐴) = (𝐺𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cfv 6343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351
This theorem is referenced by:  fveq12i  6667  fvun2  6746  fvopab3ig  6755  fvsnun1  6935  fvpr1  6943  fvpr2  6944  fvpr1g  6945  fvpr2g  6946  fvtp1  6948  fvtp2  6949  fvtp3  6950  fvtp1g  6951  fvtp2g  6952  fvtp3g  6953  fpropnf1  7017  fveqf1o  7051  ov  7287  ovigg  7288  ovg  7307  fvresex  7656  curry1  7795  curry2  7798  fsplitfpar  7810  suppsnop  7840  wfrlem5  7955  tfr2a  8027  rdgsucmptf  8060  rdgsucmptnf  8061  frsucmpt  8069  frsucmptn  8070  seqomlem1  8082  seqomlem3  8084  seqomlem4  8085  seqom0g  8088  seqomsuc  8089  unblem2  8768  inf3lemb  9085  inf3lemc  9086  trcl  9167  r10  9194  r1sucg  9195  r1limg  9197  infxpenc2  9446  aleph0  9490  alephlim  9491  alephsuc  9492  alephfplem1  9528  alephfplem2  9529  ackbij2lem3  9661  cfsmolem  9690  infpssrlem1  9723  infpssrlem2  9724  fin23lem34  9766  fin23lem35  9767  isf32lem6  9778  isf32lem7  9779  isf32lem8  9780  isf34lem5  9798  hsmexlem7  9843  axdclem2  9940  canthp1lem2  10073  wunex2  10158  wuncval2  10167  addpiord  10304  mulpiord  10305  addpqnq  10358  mulpqnq  10361  fseq1p1m1  12985  om2uz0i  13319  om2uzrdg  13328  uzrdg0i  13331  uzrdgsuci  13332  hashkf  13697  hashgval  13698  hashinf  13700  ccat1st1st  13984  revs1  14127  cats1fv  14221  shftidt  14441  cbvsum  15052  fsumss  15082  isumclim3  15114  isumsup2  15201  cbvprod  15269  fprodss  15302  iprodclim3  15354  fprodefsum  15448  ruclem4  15587  ruclem6  15588  ruclem7  15589  sadc0  15801  sadcp1  15802  sadcaddlem  15804  sadaddlem  15813  smup0  15826  smupp1  15827  algr0  15914  algrp1  15916  ndxarg  16508  strfv2d  16529  funcoppc  17145  fthepi  17198  homadm  17300  homacd  17301  prdsidlem  17943  prdsinvlem  18208  cayleylem2  18541  symggen  18598  pmtr3ncomlem1  18601  gsumval3  19027  gsumzaddlem  19041  gsumzmhm  19057  pgpfaclem1  19203  ringidval  19253  lidlval  19964  rspval  19965  lidlnegcl  19987  lpival  20018  eqcoe1ply1eq  20465  evls1val  20483  evl1val  20492  znf1o  20698  mat1dimmul  21085  mdetralt  21217  mdetunilem7  21227  decpmatid  21378  pmatcollpwscmatlem1  21397  cpmidpmat  21481  chcoeffeq  21494  restcls  21789  restntr  21790  upxp  22231  cnmetdval  23379  remetdval  23397  qdensere2  23405  pcoptcl  23629  pcopt  23630  pcopt2  23631  pcorevlem  23634  isncvsngp  23757  cnncvsabsnegdemo  23773  ovolfsval  24077  ovollb2lem  24095  ovolunlem1a  24103  ovoliunlem1  24109  ovoliun2  24113  ovolscalem1  24120  ovolicc2lem4  24127  mblvol  24137  ioombl1lem4  24168  uniioovol  24186  uniioombllem3  24192  0pval  24278  limccnp  24497  limccnp2  24498  dvcnvrelem2  24624  itgsubstlem  24654  ply1remlem  24766  plyrem  24904  qaa  24922  abelth  25039  efif1olem4  25140  eflog  25171  logef  25176  logeftb  25178  dvrelog  25231  dvlog  25245  cxpcn3  25340  efrlim  25558  eflgam  25633  wilthlem3  25658  basellem8  25676  lgsqrlem1  25933  tgcgr4  26328  krippenlem  26487  colperpexlem1  26527  opphllem3  26546  lmiisolem  26593  axlowdimlem8  26746  axlowdimlem9  26747  axlowdimlem11  26749  axlowdimlem12  26750  axlowdimlem17  26755  ushgredgedg  27022  ushgredgedgloop  27024  subgruhgredgd  27077  vtxdlfgrval  27278  vtxd0nedgb  27281  vtxdushgrfvedg  27283  vtxdginducedm1lem3  27334  finsumvtxdg2size  27343  vtxdgoddnumeven  27346  isrgr  27352  fusgrregdegfi  27362  wlk1walk  27431  wlkres  27463  wlkp1lem5  27470  wlkp1lem6  27471  wlkp1lem7  27472  wlkp1lem8  27473  clwlkcompbp  27574  crctcshwlkn0lem4  27602  crctcshwlkn0lem5  27603  crctcshwlkn0lem6  27604  2wlkdlem3  27716  2wlkdlem8  27722  2wlkond  27726  umgr2adedgwlk  27734  1wlkdlem4  27928  1pthond  27932  wlk2v2elem2  27944  3wlkdlem3  27949  3wlkdlem8  27955  3cycld  27966  3cyclpd  27967  eucrctshift  28031  frgrncvvdeq  28097  frgrwopreglem2  28101  ex-fpar  28250  avril1  28251  vafval  28389  smfval  28391  0vfval  28392  nmcvfval  28393  vsfval  28419  hhssabloilem  29047  pjoc2i  29224  pjcji  29470  ho0val  29536  hoival  29541  adjbdlnb  29870  nmopcoadji  29887  opsqrlem2  29927  opsqrlem5  29930  hmopidmchi  29937  hmopidmpji  29938  pjinvari  29977  pjadj2coi  29990  pj3lem1  29992  funcnvmpt  30423  pmtrprfv2  30764  cycpmco2lem7  30806  rgmoddim  31068  madjusmdetlem1  31152  cnre2csqlem  31210  zzsnm  31259  rrhcn  31295  qqhre  31318  oms0  31612  omsmon  31613  omssubaddlem  31614  omssubadd  31615  eulerpart  31697  fib0  31714  fib1  31715  fibp1  31716  coinflippv  31798  gsumnunsn  31868  2cycld  32442  derangenlem  32475  kur14lem2  32511  kur14lem3  32512  kur14lem5  32514  kur14lem6  32515  txsconnlem  32544  cvmliftlem4  32592  cvmliftlem5  32593  satf0sucom  32677  satf0suc  32680  satf0op  32681  fmla  32685  satffunlem2lem2  32710  satfv0fvfmla0  32717  sate0  32719  trpredmintr  33127  trpred0  33132  frrlem12  33191  fprlem1  33194  frrlem15  33199  noetalem3  33276  funpartfv  33463  fullfunfv  33465  neibastop2lem  33765  dffinxpf  34747  ftc1cnnc  35074  heiborlem4  35197  heiborlem6  35199  cdlemk13  38093  cdlemk14  38095  cdlemk15  38096  cdlemk21N  38114  cdlemk20  38115  cdlemk56w  38214  lcfrlem1  38783  hdmapfval  39068  rabdiophlem2  39659  dnnumch1  39904  aomclem6  39919  mncn0  39999  aaitgo  40022  rngunsnply  40033  cytpval  40069  dssmapntrcls  40750  binomcxplemdvsum  40979  binomcxplemnotnn0  40980  binomcxp  40981  fvcod  41783  fsumsermpt  42147  fmul01  42148  fmuldfeq  42151  fmul01lt1lem1  42152  fmul01lt1lem2  42153  lptioo2cn  42213  lptioo1cn  42214  limclner  42219  dvsinax  42481  fperdvper  42487  dvnmul  42511  dvnprodlem1  42514  dvnprodlem2  42515  dvnprodlem3  42516  itgsin0pilem1  42518  stoweidlem3  42571  stoweidlem17  42585  stoweidlem47  42615  fourierdlem42  42717  fourierdlem62  42736  fourierdlem80  42754  fourierdlem90  42764  fourierdlem92  42766  fourierdlem93  42767  fourierdlem103  42777  fourierdlem104  42778  fouriercnp  42794  sge0isum  42992  sge0seq  43011  ovnsubadd  43137  vonn0ioo  43252  vonn0icc  43253  smflimsup  43385  fundcmpsurinjimaid  43854  isomushgr  44270  rhmsubclem2  44637  rhmsubcALTVlem2  44655  ply1mulgsum  44724  lineval  44728  lincvalpr  44753  lindslinindimp2lem4  44796  zlmodzxzldeplem3  44837  zlmodzxzldeplem4  44838  itcoval0mpt  45006  ackvalsuc1mpt  45018  ackval0  45020  ackval40  45033  ackval41a  45034  ackval42  45036  ackval50  45038  ehl2eudisval0  45065  2sphere0  45090  line2  45092  line2x  45094  line2y  45095  itscnhlinecirc02p  45125
  Copyright terms: Public domain W3C validator