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

Theorem fveq1i 5713
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 5711 . 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 1369   ` cfv 5439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447
This theorem is referenced by:  fveq12i  5717  fvun2  5784  fvopab3ig  5792  fvsnun1  5934  fvsnun2  5935  fvpr1  5942  fvpr2  5943  fvpr1g  5944  fvpr2g  5945  fvtp1  5946  fvtp2  5947  fvtp3  5948  fvtp1g  5949  fvtp2g  5950  fvtp3g  5951  fveqf1o  6021  ov  6231  ovigg  6232  ovg  6250  fvresex  6571  curry1  6685  curry2  6688  suppsnop  6725  tfr2a  6875  rdgsucmptf  6905  rdgsucmptnf  6906  frsucmpt  6914  frsucmptn  6915  seqomlem1  6926  seqomlem3  6928  seqomlem4  6929  seqom0g  6932  seqomsuc  6933  unblem2  7586  inf3lemb  7852  inf3lemc  7853  trcl  7969  r10  7996  r1sucg  7997  r1limg  7999  infxpenc2  8209  infxpenc2OLD  8213  aleph0  8257  alephlim  8258  alephsuc  8259  alephfplem1  8295  alephfplem2  8296  ackbij2lem3  8431  cfsmolem  8460  infpssrlem1  8493  infpssrlem2  8494  fin23lem34  8536  fin23lem35  8537  isf32lem6  8548  isf32lem7  8549  isf32lem8  8550  isf34lem5  8568  hsmexlem7  8613  axdclem2  8710  canthp1lem2  8841  wunex2  8926  wuncval2  8935  addpiord  9074  mulpiord  9075  addpqnq  9128  mulpqnq  9131  fseq1p1m1  11555  om2uz0i  11791  om2uzrdg  11800  uzrdg0i  11803  uzrdgsuci  11804  hashkf  12126  hashgval  12127  hashinf  12129  revs1  12426  cats1fv  12507  shftidt  12592  cbvsum  13193  fsumss  13223  isumclim3  13247  isumsup2  13330  ruclem4  13537  ruclem6  13538  ruclem7  13539  sadc0  13671  sadcp1  13672  sadcaddlem  13674  sadaddlem  13683  smup0  13696  smupp1  13697  algr0  13768  algrp1  13770  ndxarg  14215  strfv2d  14227  xpsc0  14519  xpsc1  14520  funcoppc  14806  fthepi  14859  homadm  14929  homacd  14930  prdsidlem  15474  prdsinvlem  15684  cayleylem2  15939  symggen  15997  pmtr3ncomlem1  16000  gsumval3OLD  16403  gsumval3  16406  gsumzaddlem  16429  gsumzaddlemOLD  16431  gsumzmhm  16452  gsumzmhmOLD  16453  pgpfaclem1  16604  rngidval  16627  lidlval  17295  rspval  17296  lidlnegcl  17318  lpival  17349  evls1val  17777  evl1val  17785  znf1o  18006  mdetralt  18436  mdetunilem7  18446  restcls  18807  restntr  18808  upxp  19218  cnmetdval  20372  remetdval  20388  qdensere2  20396  pcoptcl  20615  pcopt  20616  pcopt2  20617  pcorevlem  20620  ovolfsval  20976  ovollb2lem  20993  ovolunlem1a  21001  ovoliunlem1  21007  ovoliun2  21011  ovolscalem1  21018  ovolicc2lem4  21025  mblvol  21035  ioombl1lem4  21064  uniioovol  21081  uniioombllem3  21087  0pval  21171  limccnp  21388  limccnp2  21389  dvcnvrelem2  21512  itgsubstlem  21542  ply1remlem  21656  plyrem  21793  qaa  21811  abelth  21928  efif1olem4  22023  eflog  22050  logef  22052  logeftb  22054  dvrelog  22104  dvlog  22118  cxpcn3  22208  efrlim  22385  wilthlem3  22430  basellem8  22447  lgsqrlem1  22702  krippenlem  23106  colperplem1  23134  axlowdimlem8  23217  axlowdimlem9  23218  axlowdimlem11  23220  axlowdimlem12  23221  axlowdimlem17  23226  2wlklemA  23475  2wlklemB  23476  2wlklemC  23477  wlkntrllem2  23481  wlkntrllem3  23482  constr3lem4  23555  constr3lem5  23556  vdgr1c  23597  eupares  23618  eupap1  23619  vdegp1ai  23627  vdegp1bi  23628  avril1  23678  vafval  24003  smfval  24005  0vfval  24006  nmcvfval  24007  vsfval  24035  pjoc2i  24863  pjcji  25109  ho0val  25176  hoival  25181  adjbdlnb  25510  nmopcoadji  25527  opsqrlem2  25567  opsqrlem5  25570  hmopidmchi  25577  hmopidmpji  25578  pjinvari  25617  pjadj2coi  25630  pj3lem1  25632  funcnvmptOLD  26008  funcnvmpt  26009  cnre2csqlem  26362  zzsnm  26411  zzsnmOLD  26412  rrhcn  26448  qqhre  26468  oms0  26732  omsmon  26733  eulerpart  26787  fib0  26804  fib1  26805  fibp1  26806  coinflippv  26888  gsumnunsn  26959  eflgam  27053  derangenlem  27081  kur14lem2  27117  kur14lem3  27118  kur14lem5  27120  kur14lem6  27121  txsconlem  27151  cvmliftlem4  27199  cvmliftlem5  27200  cbvprod  27450  fprodss  27483  fprodefsum  27507  iprodclim3  27522  trpredmintr  27717  trpred0  27722  wfrlem5  27750  frrlem5  27794  funpartfv  27998  fullfunfv  28000  ftc1cnnc  28492  neibastop2lem  28607  heiborlem4  28739  heiborlem6  28741  rabdiophlem2  29166  dnnumch1  29423  aomclem6  29438  mncn0  29522  aaitgo  29545  rngunsnply  29556  cytpval  29603  fmul01  29787  fmuldfeq  29790  fmul01lt1lem1  29791  fmul01lt1lem2  29792  itgsin0pilem1  29816  stoweidlem3  29824  stoweidlem17  29838  stoweidlem47  29868  wlkiswwlksur  30377  eqcoe1ply1eq  30868  ply1mulgsum  30881  lineval  30890  mat1dimmul  30911  lincvalpr  30949  lindslinindimp2lem4  30992  zlmodzxzldeplem3  31041  zlmodzxzldeplem4  31042  pmatcollpw1id  31114  cdlemk13  34592  cdlemk14  34594  cdlemk15  34595  cdlemk21N  34613  cdlemk20  34614  cdlemk56w  34713  lcfrlem1  35283  hdmapfval  35571
  Copyright terms: Public domain W3C validator