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

Theorem fveq1i 5857
Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
fveq1i.1  |-  F  =  G
Assertion
Ref Expression
fveq1i  |-  ( F `
 A )  =  ( G `  A
)

Proof of Theorem fveq1i
StepHypRef Expression
1 fveq1i.1 . 2  |-  F  =  G
2 fveq1 5855 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2ax-mp 5 1  |-  ( F `
 A )  =  ( G `  A
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586
This theorem is referenced by:  fveq12i  5861  fvun2  5930  fvopab3ig  5938  fvsnun1  6091  fvsnun2  6092  fvpr1  6099  fvpr2  6100  fvpr1g  6101  fvpr2g  6102  fvtp1  6103  fvtp2  6104  fvtp3  6105  fvtp1g  6106  fvtp2g  6107  fvtp3g  6108  fveqf1o  6190  ov  6407  ovigg  6408  ovg  6426  fvresex  6758  curry1  6877  curry2  6880  suppsnop  6917  tfr2a  7066  rdgsucmptf  7096  rdgsucmptnf  7097  frsucmpt  7105  frsucmptn  7106  seqomlem1  7117  seqomlem3  7119  seqomlem4  7120  seqom0g  7123  seqomsuc  7124  unblem2  7775  inf3lemb  8045  inf3lemc  8046  trcl  8162  r10  8189  r1sucg  8190  r1limg  8192  infxpenc2  8402  infxpenc2OLD  8406  aleph0  8450  alephlim  8451  alephsuc  8452  alephfplem1  8488  alephfplem2  8489  ackbij2lem3  8624  cfsmolem  8653  infpssrlem1  8686  infpssrlem2  8687  fin23lem34  8729  fin23lem35  8730  isf32lem6  8741  isf32lem7  8742  isf32lem8  8743  isf34lem5  8761  hsmexlem7  8806  axdclem2  8903  canthp1lem2  9034  wunex2  9119  wuncval2  9128  addpiord  9265  mulpiord  9266  addpqnq  9319  mulpqnq  9322  fseq1p1m1  11762  om2uz0i  12039  om2uzrdg  12048  uzrdg0i  12051  uzrdgsuci  12052  hashkf  12388  hashgval  12389  hashinf  12391  revs1  12720  cats1fv  12805  shftidt  12896  cbvsum  13498  fsumss  13528  isumclim3  13555  isumsup2  13639  cbvprod  13703  fprodss  13736  iprodclim3  13774  fprodefsum  13811  ruclem4  13948  ruclem6  13949  ruclem7  13950  sadc0  14085  sadcp1  14086  sadcaddlem  14088  sadaddlem  14097  smup0  14110  smupp1  14111  algr0  14182  algrp1  14184  ndxarg  14633  strfv2d  14645  xpsc0  14938  xpsc1  14939  funcoppc  15222  fthepi  15275  homadm  15345  homacd  15346  prdsidlem  15930  prdsinvlem  16156  cayleylem2  16416  symggen  16473  pmtr3ncomlem1  16476  gsumval3OLD  16886  gsumval3  16889  gsumzaddlem  16912  gsumzaddlemOLD  16914  gsumzmhm  16935  gsumzmhmOLD  16936  pgpfaclem1  17110  ringidval  17133  lidlval  17816  rspval  17817  lidlnegcl  17839  lpival  17871  eqcoe1ply1eq  18317  evls1val  18335  evl1val  18343  znf1o  18567  mat1dimmul  18955  mdetralt  19087  mdetunilem7  19097  decpmatid  19248  pmatcollpwscmatlem1  19267  cpmidpmat  19351  chcoeffeq  19364  restcls  19659  restntr  19660  upxp  20101  cnmetdval  21255  remetdval  21271  qdensere2  21279  pcoptcl  21498  pcopt  21499  pcopt2  21500  pcorevlem  21503  ovolfsval  21859  ovollb2lem  21876  ovolunlem1a  21884  ovoliunlem1  21890  ovoliun2  21894  ovolscalem1  21901  ovolicc2lem4  21908  mblvol  21918  ioombl1lem4  21948  uniioovol  21965  uniioombllem3  21971  0pval  22055  limccnp  22272  limccnp2  22273  dvcnvrelem2  22396  itgsubstlem  22426  ply1remlem  22540  plyrem  22677  qaa  22695  abelth  22812  efif1olem4  22908  eflog  22940  logef  22942  logeftb  22944  dvrelog  22994  dvlog  23008  cxpcn3  23098  efrlim  23275  wilthlem3  23320  basellem8  23337  lgsqrlem1  23592  krippenlem  24043  colperpexlem1  24080  opphllem3  24097  lmiisolem  24137  axlowdimlem8  24228  axlowdimlem9  24229  axlowdimlem11  24231  axlowdimlem12  24232  axlowdimlem17  24237  2wlklemA  24532  2wlklemB  24533  2wlklemC  24534  wlkntrllem2  24538  wlkntrllem3  24539  constr3lem4  24623  constr3lem5  24624  wlkiswwlksur  24695  vdgr1c  24881  eupares  24951  eupap1  24952  vdegp1ai  24960  vdegp1bi  24961  avril1  25147  vafval  25472  smfval  25474  0vfval  25475  nmcvfval  25476  vsfval  25504  pjoc2i  26332  pjcji  26578  ho0val  26645  hoival  26650  adjbdlnb  26979  nmopcoadji  26996  opsqrlem2  27036  opsqrlem5  27039  hmopidmchi  27046  hmopidmpji  27047  pjinvari  27086  pjadj2coi  27099  pj3lem1  27101  funcnvmptOLD  27485  funcnvmpt  27486  cnre2csqlem  27869  zzsnm  27918  zzsnmOLD  27919  rrhcn  27955  qqhre  27975  oms0  28243  omsmon  28244  eulerpart  28298  fib0  28315  fib1  28316  fibp1  28317  coinflippv  28399  gsumnunsn  28470  eflgam  28564  derangenlem  28592  kur14lem2  28628  kur14lem3  28629  kur14lem5  28631  kur14lem6  28632  txsconlem  28662  cvmliftlem4  28710  cvmliftlem5  28711  trpredmintr  29289  trpred0  29294  wfrlem5  29322  frrlem5  29366  funpartfv  29570  fullfunfv  29572  ftc1cnnc  30064  neibastop2lem  30153  heiborlem4  30285  heiborlem6  30287  rabdiophlem2  30710  dnnumch1  30965  aomclem6  30980  mncn0  31064  aaitgo  31087  rngunsnply  31098  cytpval  31145  fmul01  31502  fmuldfeq  31505  fmul01lt1lem1  31506  fmul01lt1lem2  31507  lptioo2cn  31559  lptioo1cn  31560  limclner  31565  dvsinax  31612  fperdvper  31619  itgsin0pilem1  31638  stoweidlem3  31674  stoweidlem17  31688  stoweidlem47  31718  fourierdlem42  31820  fourierdlem62  31840  fourierdlem80  31858  fourierdlem90  31868  fourierdlem92  31870  fourierdlem93  31871  fourierdlem103  31881  fourierdlem104  31882  fouriercnp  31898  rhmsubclem2  32628  rhmsubcOLDlem2  32647  ply1mulgsum  32725  lineval  32729  lincvalpr  32754  lindslinindimp2lem4  32797  zlmodzxzldeplem3  32838  zlmodzxzldeplem4  32839  cdlemk13  36318  cdlemk14  36320  cdlemk15  36321  cdlemk21N  36339  cdlemk20  36340  cdlemk56w  36439  lcfrlem1  37009  hdmapfval  37297
  Copyright terms: Public domain W3C validator