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

Theorem fveq1i 6345
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 6343 . 2 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
31, 2ax-mp 5 1 (𝐹𝐴) = (𝐺𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624  cfv 6041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049
This theorem is referenced by:  fveq12i  6349  fvun2  6424  fvopab3ig  6432  fvsnun1  6604  fvsnun2  6605  fvpr1  6612  fvpr2  6613  fvpr1g  6614  fvpr2g  6615  fvtp1  6616  fvtp2  6617  fvtp3  6618  fvtp1g  6619  fvtp2g  6620  fvtp3g  6621  fpropnf1  6679  fveqf1o  6712  ov  6937  ovigg  6938  ovg  6956  fvresex  7296  curry1  7429  curry2  7432  suppsnop  7469  wfrlem5  7580  tfr2a  7652  rdgsucmptf  7685  rdgsucmptnf  7686  frsucmpt  7694  frsucmptn  7695  seqomlem1  7706  seqomlem3  7708  seqomlem4  7709  seqom0g  7712  seqomsuc  7713  unblem2  8370  inf3lemb  8687  inf3lemc  8688  trcl  8769  r10  8796  r1sucg  8797  r1limg  8799  infxpenc2  9027  aleph0  9071  alephlim  9072  alephsuc  9073  alephfplem1  9109  alephfplem2  9110  ackbij2lem3  9247  cfsmolem  9276  infpssrlem1  9309  infpssrlem2  9310  fin23lem34  9352  fin23lem35  9353  isf32lem6  9364  isf32lem7  9365  isf32lem8  9366  isf34lem5  9384  hsmexlem7  9429  axdclem2  9526  canthp1lem2  9659  wunex2  9744  wuncval2  9753  addpiord  9890  mulpiord  9891  addpqnq  9944  mulpqnq  9947  fseq1p1m1  12599  om2uz0i  12932  om2uzrdg  12941  uzrdg0i  12944  uzrdgsuci  12945  hashkf  13305  hashgval  13306  hashinf  13308  ccat1st1st  13594  revs1  13706  cats1fv  13796  shftidt  14013  cbvsum  14616  fsumss  14647  isumclim3  14681  isumsup2  14769  cbvprod  14836  fprodss  14869  iprodclim3  14922  fprodefsum  15016  ruclem4  15154  ruclem6  15155  ruclem7  15156  sadc0  15370  sadcp1  15371  sadcaddlem  15373  sadaddlem  15382  smup0  15395  smupp1  15396  algr0  15479  algrp1  15481  ndxarg  16076  strfv2d  16099  xpsc0  16414  xpsc1  16415  funcoppc  16728  fthepi  16781  homadm  16883  homacd  16884  prdsidlem  17515  prdsinvlem  17717  cayleylem2  18025  symggen  18082  pmtr3ncomlem1  18085  gsumval3  18500  gsumzaddlem  18513  gsumzmhm  18529  pgpfaclem1  18672  ringidval  18695  lidlval  19386  rspval  19387  lidlnegcl  19408  lpival  19439  eqcoe1ply1eq  19861  evls1val  19879  evl1val  19887  znf1o  20094  mat1dimmul  20476  mdetralt  20608  mdetunilem7  20618  decpmatid  20769  pmatcollpwscmatlem1  20788  cpmidpmat  20872  chcoeffeq  20885  restcls  21179  restntr  21180  upxp  21620  cnmetdval  22767  remetdval  22785  qdensere2  22793  pcoptcl  23013  pcopt  23014  pcopt2  23015  pcorevlem  23018  isncvsngp  23141  cnncvsabsnegdemo  23157  ovolfsval  23431  ovollb2lem  23448  ovolunlem1a  23456  ovoliunlem1  23462  ovoliun2  23466  ovolscalem1  23473  ovolicc2lem4  23480  mblvol  23490  ioombl1lem4  23521  uniioovol  23539  uniioombllem3  23545  0pval  23629  limccnp  23846  limccnp2  23847  dvcnvrelem2  23972  itgsubstlem  24002  ply1remlem  24113  plyrem  24251  qaa  24269  abelth  24386  efif1olem4  24482  eflog  24514  logef  24519  logeftb  24521  dvrelog  24574  dvlog  24588  cxpcn3  24680  efrlim  24887  eflgam  24962  wilthlem3  24987  basellem8  25005  lgsqrlem1  25262  tgcgr4  25617  krippenlem  25776  colperpexlem1  25813  opphllem3  25832  lmiisolem  25879  axlowdimlem8  26020  axlowdimlem9  26021  axlowdimlem11  26023  axlowdimlem12  26024  axlowdimlem17  26029  ushgredgedg  26312  ushgredgedgloop  26314  subgruhgredgd  26367  vtxdlfgrval  26583  vtxd0nedgb  26586  vtxdushgrfvedg  26588  vtxdginducedm1lem3  26639  finsumvtxdg2size  26648  vtxdgoddnumeven  26651  isrgr  26657  fusgrregdegfi  26667  wlk1walk  26737  wlkres  26769  wlkp1lem5  26776  wlkp1lem6  26777  wlkp1lem7  26778  wlkp1lem8  26779  clwlkcompbp  26880  crctcshwlkn0lem4  26908  crctcshwlkn0lem5  26909  crctcshwlkn0lem6  26910  wlkwwlksur  26998  2wlkdlem3  27039  2wlkdlem8  27045  2wlkond  27049  umgr2adedgwlk  27057  1wlkdlem4  27284  1pthond  27288  wlk2v2elem2  27300  3wlkdlem3  27305  3wlkdlem8  27311  3cycld  27322  3cyclpd  27323  eucrctshift  27387  frgrncvvdeq  27455  frgrwopreglem2  27459  avril1  27622  vafval  27759  smfval  27761  0vfval  27762  nmcvfval  27763  vsfval  27789  hhssabloilem  28419  pjoc2i  28598  pjcji  28844  ho0val  28910  hoival  28915  adjbdlnb  29244  nmopcoadji  29261  opsqrlem2  29301  opsqrlem5  29304  hmopidmchi  29311  hmopidmpji  29312  pjinvari  29351  pjadj2coi  29364  pj3lem1  29366  funcnvmptOLD  29768  funcnvmpt  29769  pmtrprfv2  30149  madjusmdetlem1  30194  cnre2csqlem  30257  zzsnm  30306  rrhcn  30342  qqhre  30365  oms0  30660  omsmon  30661  omssubaddlem  30662  omssubadd  30663  eulerpart  30745  fib0  30762  fib1  30763  fibp1  30764  coinflippv  30846  gsumnunsn  30916  derangenlem  31452  kur14lem2  31488  kur14lem3  31489  kur14lem5  31491  kur14lem6  31492  txsconnlem  31521  cvmliftlem4  31569  cvmliftlem5  31570  trpredmintr  32028  trpred0  32033  frrlem5  32082  noetalem3  32163  funpartfv  32350  fullfunfv  32352  neibastop2lem  32653  dffinxpf  33525  ftc1cnnc  33789  heiborlem4  33918  heiborlem6  33920  cdlemk13  36634  cdlemk14  36636  cdlemk15  36637  cdlemk21N  36655  cdlemk20  36656  cdlemk56w  36755  lcfrlem1  37325  hdmapfval  37613  rabdiophlem2  37860  dnnumch1  38108  aomclem6  38123  mncn0  38203  aaitgo  38226  rngunsnply  38237  cytpval  38281  dssmapntrcls  38920  binomcxplemdvsum  39048  binomcxplemnotnn0  39049  binomcxp  39050  fvcod  39914  fsumsermpt  40306  fmul01  40307  fmuldfeq  40310  fmul01lt1lem1  40311  fmul01lt1lem2  40312  lptioo2cn  40372  lptioo1cn  40373  limclner  40378  dvsinax  40622  fperdvper  40628  dvnmul  40653  dvnprodlem1  40656  dvnprodlem2  40657  dvnprodlem3  40658  itgsin0pilem1  40660  stoweidlem3  40715  stoweidlem17  40729  stoweidlem47  40759  fourierdlem42  40861  fourierdlem62  40880  fourierdlem80  40898  fourierdlem90  40908  fourierdlem92  40910  fourierdlem93  40911  fourierdlem103  40921  fourierdlem104  40922  fouriercnp  40938  sge0isum  41139  sge0seq  41158  ovnsubadd  41284  vonn0ioo  41399  vonn0icc  41400  smflimsup  41532  rhmsubclem2  42589  rhmsubcALTVlem2  42607  ply1mulgsum  42680  lineval  42684  lincvalpr  42709  lindslinindimp2lem4  42752  zlmodzxzldeplem3  42793  zlmodzxzldeplem4  42794
  Copyright terms: Public domain W3C validator