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 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-uni 4223  df-br 4427  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  7048  tfr2a  7121  rdgsucmptf  7154  rdgsucmptnf  7155  frsucmpt  7163  frsucmptn  7164  seqomlem1  7175  seqomlem3  7177  seqomlem4  7178  seqom0g  7181  seqomsuc  7182  unblem2  7830  inf3lemb  8130  inf3lemc  8131  trcl  8211  r10  8238  r1sucg  8239  r1limg  8241  infxpenc2  8451  aleph0  8495  alephlim  8496  alephsuc  8497  alephfplem1  8533  alephfplem2  8534  ackbij2lem3  8669  cfsmolem  8698  infpssrlem1  8731  infpssrlem2  8732  fin23lem34  8774  fin23lem35  8775  isf32lem6  8786  isf32lem7  8787  isf32lem8  8788  isf34lem5  8806  hsmexlem7  8851  axdclem2  8948  canthp1lem2  9077  wunex2  9162  wuncval2  9171  addpiord  9308  mulpiord  9309  addpqnq  9362  mulpqnq  9365  fseq1p1m1  11866  om2uz0i  12158  om2uzrdg  12167  uzrdg0i  12170  uzrdgsuci  12171  hashkf  12514  hashgval  12515  hashinf  12517  revs1  12855  cats1fv  12940  shftidt  13124  cbvsum  13739  fsumss  13769  isumclim3  13798  isumsup2  13882  cbvprod  13947  fprodss  13980  iprodclim3  14031  fprodefsum  14127  ruclem4  14264  ruclem6  14265  ruclem7  14266  sadc0  14402  sadcp1  14403  sadcaddlem  14405  sadaddlem  14414  smup0  14427  smupp1  14428  algr0  14502  algrp1  14504  ndxarg  15104  strfv2d  15118  xpsc0  15417  xpsc1  15418  funcoppc  15731  fthepi  15784  homadm  15886  homacd  15887  prdsidlem  16519  prdsinvlem  16745  cayleylem2  17005  symggen  17062  pmtr3ncomlem1  17065  gsumval3  17476  gsumzaddlem  17489  gsumzmhm  17505  pgpfaclem1  17649  ringidval  17672  lidlval  18350  rspval  18351  lidlnegcl  18372  lpival  18404  eqcoe1ply1eq  18826  evls1val  18844  evl1val  18852  znf1o  19053  mat1dimmul  19432  mdetralt  19564  mdetunilem7  19574  decpmatid  19725  pmatcollpwscmatlem1  19744  cpmidpmat  19828  chcoeffeq  19841  restcls  20128  restntr  20129  upxp  20569  cnmetdval  21702  remetdval  21718  qdensere2  21726  pcoptcl  21945  pcopt  21946  pcopt2  21947  pcorevlem  21950  ovolfsval  22302  ovollb2lem  22319  ovolunlem1a  22327  ovoliunlem1  22333  ovoliun2  22337  ovolscalem1  22344  ovolicc2lem4  22351  mblvol  22361  ioombl1lem4  22391  uniioovol  22413  uniioombllem3  22420  0pval  22506  limccnp  22723  limccnp2  22724  dvcnvrelem2  22847  itgsubstlem  22877  ply1remlem  22988  plyrem  23126  qaa  23144  abelth  23261  efif1olem4  23359  eflog  23391  logef  23396  logeftb  23398  dvrelog  23447  dvlog  23461  cxpcn3  23553  efrlim  23760  eflgam  23835  wilthlem3  23860  basellem8  23877  lgsqrlem1  24132  krippenlem  24592  colperpexlem1  24629  opphllem3  24648  lmiisolem  24694  axlowdimlem8  24825  axlowdimlem9  24826  axlowdimlem11  24828  axlowdimlem12  24829  axlowdimlem17  24834  2wlklemA  25129  2wlklemB  25130  2wlklemC  25131  wlkntrllem2  25135  wlkntrllem3  25136  constr3lem4  25220  constr3lem5  25221  wlkiswwlksur  25292  vdgr1c  25478  eupares  25548  eupap1  25549  vdegp1ai  25557  vdegp1bi  25558  avril1  25745  vafval  26067  smfval  26069  0vfval  26070  nmcvfval  26071  vsfval  26099  pjoc2i  26926  pjcji  27172  ho0val  27238  hoival  27243  adjbdlnb  27572  nmopcoadji  27589  opsqrlem2  27629  opsqrlem5  27632  hmopidmchi  27639  hmopidmpji  27640  pjinvari  27679  pjadj2coi  27692  pj3lem1  27694  funcnvmptOLD  28110  funcnvmpt  28111  pmtrprfv2  28450  madjusmdetlem1  28492  cnre2csqlem  28555  zzsnm  28604  rrhcn  28640  qqhre  28663  oms0  28958  omsmon  28959  omssubaddlem  28960  omssubadd  28961  eulerpart  29041  fib0  29058  fib1  29059  fibp1  29060  coinflippv  29142  gsumnunsn  29213  derangenlem  29682  kur14lem2  29718  kur14lem3  29719  kur14lem5  29721  kur14lem6  29722  txsconlem  29751  cvmliftlem4  29799  cvmliftlem5  29800  trpredmintr  30259  trpred0  30264  frrlem5  30305  funpartfv  30497  fullfunfv  30499  neibastop2lem  30801  ftc1cnnc  31719  heiborlem4  31849  heiborlem6  31851  cdlemk13  34127  cdlemk14  34129  cdlemk15  34130  cdlemk21N  34148  cdlemk20  34149  cdlemk56w  34248  lcfrlem1  34818  hdmapfval  35106  rabdiophlem2  35353  dnnumch1  35607  aomclem6  35622  mncn0  35703  aaitgo  35726  rngunsnply  35737  cytpval  35784  binomcxplemdvsum  36340  binomcxplemnotnn0  36341  binomcxp  36342  fmul01  37229  fmuldfeq  37232  fmul01lt1lem1  37233  fmul01lt1lem2  37234  lptioo2cn  37297  lptioo1cn  37298  limclner  37303  dvsinax  37354  fperdvper  37361  dvnmul  37386  dvnprodlem1  37389  dvnprodlem2  37390  dvnprodlem3  37391  itgsin0pilem1  37394  stoweidlem3  37431  stoweidlem17  37445  stoweidlem47  37476  fourierdlem42  37579  fourierdlem62  37599  fourierdlem80  37617  fourierdlem90  37627  fourierdlem92  37629  fourierdlem93  37630  fourierdlem103  37640  fourierdlem104  37641  fouriercnp  37657  rhmsubclem2  38846  rhmsubcALTVlem2  38865  ply1mulgsum  38941  lineval  38945  lincvalpr  38970  lindslinindimp2lem4  39013  zlmodzxzldeplem3  39054  zlmodzxzldeplem4  39055
  Copyright terms: Public domain W3C validator