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

Theorem fveq1i 5882
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 5880 . 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 1437   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rex 2777  df-uni 4220  df-br 4424  df-iota 5565  df-fv 5609
This theorem is referenced by:  fveq12i  5886  fvun2  5953  fvopab3ig  5961  fvsnun1  6114  fvsnun2  6115  fvpr1  6122  fvpr2  6123  fvpr1g  6124  fvpr2g  6125  fvtp1  6126  fvtp2  6127  fvtp3  6128  fvtp1g  6129  fvtp2g  6130  fvtp3g  6131  fveqf1o  6215  ov  6430  ovigg  6431  ovg  6449  fvresex  6780  curry1  6899  curry2  6902  suppsnop  6939  wfrlem5  7051  tfr2a  7124  rdgsucmptf  7157  rdgsucmptnf  7158  frsucmpt  7166  frsucmptn  7167  seqomlem1  7178  seqomlem3  7180  seqomlem4  7181  seqom0g  7184  seqomsuc  7185  unblem2  7833  inf3lemb  8139  inf3lemc  8140  trcl  8220  r10  8247  r1sucg  8248  r1limg  8250  infxpenc2  8460  aleph0  8504  alephlim  8505  alephsuc  8506  alephfplem1  8542  alephfplem2  8543  ackbij2lem3  8678  cfsmolem  8707  infpssrlem1  8740  infpssrlem2  8741  fin23lem34  8783  fin23lem35  8784  isf32lem6  8795  isf32lem7  8796  isf32lem8  8797  isf34lem5  8815  hsmexlem7  8860  axdclem2  8957  canthp1lem2  9085  wunex2  9170  wuncval2  9179  addpiord  9316  mulpiord  9317  addpqnq  9370  mulpqnq  9373  fseq1p1m1  11875  om2uz0i  12167  om2uzrdg  12176  uzrdg0i  12179  uzrdgsuci  12180  hashkf  12523  hashgval  12524  hashinf  12526  revs1  12872  cats1fv  12957  shftidt  13145  cbvsum  13760  fsumss  13790  isumclim3  13819  isumsup2  13903  cbvprod  13968  fprodss  14001  iprodclim3  14052  fprodefsum  14148  ruclem4  14285  ruclem6  14286  ruclem7  14287  sadc0  14427  sadcp1  14428  sadcaddlem  14430  sadaddlem  14439  smup0  14452  smupp1  14453  algr0  14530  algrp1  14532  ndxarg  15140  strfv2d  15154  xpsc0  15465  xpsc1  15466  funcoppc  15779  fthepi  15832  homadm  15934  homacd  15935  prdsidlem  16567  prdsinvlem  16793  cayleylem2  17053  symggen  17110  pmtr3ncomlem1  17113  gsumval3  17540  gsumzaddlem  17553  gsumzmhm  17569  pgpfaclem1  17713  ringidval  17736  lidlval  18414  rspval  18415  lidlnegcl  18436  lpival  18468  eqcoe1ply1eq  18890  evls1val  18908  evl1val  18916  znf1o  19120  mat1dimmul  19499  mdetralt  19631  mdetunilem7  19641  decpmatid  19792  pmatcollpwscmatlem1  19811  cpmidpmat  19895  chcoeffeq  19908  restcls  20195  restntr  20196  upxp  20636  cnmetdval  21789  remetdval  21805  qdensere2  21813  pcoptcl  22050  pcopt  22051  pcopt2  22052  pcorevlem  22055  ovolfsval  22421  ovollb2lem  22439  ovolunlem1a  22447  ovoliunlem1  22453  ovoliun2  22457  ovolscalem1  22464  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  mblvol  22482  ioombl1lem4  22512  uniioovol  22534  uniioombllem3  22541  0pval  22627  limccnp  22844  limccnp2  22845  dvcnvrelem2  22968  itgsubstlem  22998  ply1remlem  23111  plyrem  23256  qaa  23277  abelth  23394  efif1olem4  23492  eflog  23524  logef  23529  logeftb  23531  dvrelog  23580  dvlog  23594  cxpcn3  23686  efrlim  23893  eflgam  23968  wilthlem3  23993  basellem8  24012  lgsqrlem1  24267  tgcgr4  24574  krippenlem  24733  colperpexlem1  24770  opphllem3  24789  lmiisolem  24836  axlowdimlem8  24977  axlowdimlem9  24978  axlowdimlem11  24980  axlowdimlem12  24981  axlowdimlem17  24986  2wlklemA  25282  2wlklemB  25283  2wlklemC  25284  wlkntrllem2  25288  wlkntrllem3  25289  constr3lem4  25373  constr3lem5  25374  wlkiswwlksur  25445  vdgr1c  25631  eupares  25701  eupap1  25702  vdegp1ai  25710  vdegp1bi  25711  avril1  25898  vafval  26220  smfval  26222  0vfval  26223  nmcvfval  26224  vsfval  26252  pjoc2i  27089  pjcji  27335  ho0val  27401  hoival  27406  adjbdlnb  27735  nmopcoadji  27752  opsqrlem2  27792  opsqrlem5  27795  hmopidmchi  27802  hmopidmpji  27803  pjinvari  27842  pjadj2coi  27855  pj3lem1  27857  funcnvmptOLD  28272  funcnvmpt  28273  pmtrprfv2  28619  madjusmdetlem1  28661  cnre2csqlem  28724  zzsnm  28773  rrhcn  28809  qqhre  28832  oms0  29133  omsmon  29134  omssubaddlem  29135  omssubadd  29136  oms0OLD  29137  omsmonOLD  29138  omssubaddlemOLD  29139  omssubaddOLD  29140  eulerpart  29223  fib0  29240  fib1  29241  fibp1  29242  coinflippv  29324  gsumnunsn  29433  derangenlem  29902  kur14lem2  29938  kur14lem3  29939  kur14lem5  29941  kur14lem6  29942  txsconlem  29971  cvmliftlem4  30019  cvmliftlem5  30020  trpredmintr  30479  trpred0  30484  frrlem5  30525  funpartfv  30717  fullfunfv  30719  neibastop2lem  31021  dffinxpf  31741  ftc1cnnc  31980  heiborlem4  32110  heiborlem6  32112  cdlemk13  34388  cdlemk14  34390  cdlemk15  34391  cdlemk21N  34409  cdlemk20  34410  cdlemk56w  34509  lcfrlem1  35079  hdmapfval  35367  rabdiophlem2  35614  dnnumch1  35872  aomclem6  35887  mncn0  35968  aaitgo  35998  rngunsnply  36009  cytpval  36056  binomcxplemdvsum  36674  binomcxplemnotnn0  36675  binomcxp  36676  fmul01  37598  fmuldfeq  37601  fmul01lt1lem1  37602  fmul01lt1lem2  37603  lptioo2cn  37666  lptioo1cn  37667  limclner  37672  dvsinax  37723  fperdvper  37730  dvnmul  37758  dvnprodlem1  37761  dvnprodlem2  37762  dvnprodlem3  37763  itgsin0pilem1  37766  stoweidlem3  37803  stoweidlem17  37817  stoweidlem47  37848  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem62  37972  fourierdlem80  37990  fourierdlem90  38000  fourierdlem92  38002  fourierdlem93  38003  fourierdlem103  38013  fourierdlem104  38014  fouriercnp  38030  sge0isum  38177  ovnsubadd  38298  usgredgedga  39091  subgruhgredgd  39130  rhmsubclem2  39709  rhmsubcALTVlem2  39728  ply1mulgsum  39804  lineval  39808  lincvalpr  39833  lindslinindimp2lem4  39876  zlmodzxzldeplem3  39917  zlmodzxzldeplem4  39918
  Copyright terms: Public domain W3C validator