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

Theorem fveq1i 5893
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 5891 . 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 1455   ` cfv 5605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-uni 4213  df-br 4419  df-iota 5569  df-fv 5613
This theorem is referenced by:  fveq12i  5897  fvun2  5965  fvopab3ig  5973  fvsnun1  6128  fvsnun2  6129  fvpr1  6136  fvpr2  6137  fvpr1g  6138  fvpr2g  6139  fvtp1  6140  fvtp2  6141  fvtp3  6142  fvtp1g  6143  fvtp2g  6144  fvtp3g  6145  fveqf1o  6230  ov  6448  ovigg  6449  ovg  6467  fvresex  6798  curry1  6920  curry2  6923  suppsnop  6960  wfrlem5  7071  tfr2a  7144  rdgsucmptf  7177  rdgsucmptnf  7178  frsucmpt  7186  frsucmptn  7187  seqomlem1  7198  seqomlem3  7200  seqomlem4  7201  seqom0g  7204  seqomsuc  7205  unblem2  7855  inf3lemb  8161  inf3lemc  8162  trcl  8243  r10  8270  r1sucg  8271  r1limg  8273  infxpenc2  8484  aleph0  8528  alephlim  8529  alephsuc  8530  alephfplem1  8566  alephfplem2  8567  ackbij2lem3  8702  cfsmolem  8731  infpssrlem1  8764  infpssrlem2  8765  fin23lem34  8807  fin23lem35  8808  isf32lem6  8819  isf32lem7  8820  isf32lem8  8821  isf34lem5  8839  hsmexlem7  8884  axdclem2  8981  canthp1lem2  9109  wunex2  9194  wuncval2  9203  addpiord  9340  mulpiord  9341  addpqnq  9394  mulpqnq  9397  fseq1p1m1  11903  om2uz0i  12199  om2uzrdg  12208  uzrdg0i  12211  uzrdgsuci  12212  hashkf  12555  hashgval  12556  hashinf  12558  revs1  12913  cats1fv  12998  shftidt  13200  cbvsum  13816  fsumss  13846  isumclim3  13875  isumsup2  13959  cbvprod  14024  fprodss  14057  iprodclim3  14108  fprodefsum  14204  ruclem4  14341  ruclem6  14342  ruclem7  14343  sadc0  14483  sadcp1  14484  sadcaddlem  14486  sadaddlem  14495  smup0  14508  smupp1  14509  algr0  14586  algrp1  14588  ndxarg  15196  strfv2d  15210  xpsc0  15521  xpsc1  15522  funcoppc  15835  fthepi  15888  homadm  15990  homacd  15991  prdsidlem  16623  prdsinvlem  16849  cayleylem2  17109  symggen  17166  pmtr3ncomlem1  17169  gsumval3  17596  gsumzaddlem  17609  gsumzmhm  17625  pgpfaclem1  17769  ringidval  17792  lidlval  18470  rspval  18471  lidlnegcl  18492  lpival  18524  eqcoe1ply1eq  18946  evls1val  18964  evl1val  18972  znf1o  19177  mat1dimmul  19556  mdetralt  19688  mdetunilem7  19698  decpmatid  19849  pmatcollpwscmatlem1  19868  cpmidpmat  19952  chcoeffeq  19965  restcls  20252  restntr  20253  upxp  20693  cnmetdval  21846  remetdval  21862  qdensere2  21870  pcoptcl  22107  pcopt  22108  pcopt2  22109  pcorevlem  22112  ovolfsval  22478  ovollb2lem  22496  ovolunlem1a  22504  ovoliunlem1  22510  ovoliun2  22514  ovolscalem1  22521  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  mblvol  22539  ioombl1lem4  22570  uniioovol  22592  uniioombllem3  22599  0pval  22685  limccnp  22902  limccnp2  22903  dvcnvrelem2  23026  itgsubstlem  23056  ply1remlem  23169  plyrem  23314  qaa  23335  abelth  23452  efif1olem4  23550  eflog  23582  logef  23587  logeftb  23589  dvrelog  23638  dvlog  23652  cxpcn3  23744  efrlim  23951  eflgam  24026  wilthlem3  24051  basellem8  24070  lgsqrlem1  24325  tgcgr4  24632  krippenlem  24791  colperpexlem1  24828  opphllem3  24847  lmiisolem  24894  axlowdimlem8  25035  axlowdimlem9  25036  axlowdimlem11  25038  axlowdimlem12  25039  axlowdimlem17  25044  2wlklemA  25340  2wlklemB  25341  2wlklemC  25342  wlkntrllem2  25346  wlkntrllem3  25347  constr3lem4  25431  constr3lem5  25432  wlkiswwlksur  25503  vdgr1c  25689  eupares  25759  eupap1  25760  vdegp1ai  25768  vdegp1bi  25769  avril1  25956  vafval  26278  smfval  26280  0vfval  26281  nmcvfval  26282  vsfval  26310  pjoc2i  27147  pjcji  27393  ho0val  27459  hoival  27464  adjbdlnb  27793  nmopcoadji  27810  opsqrlem2  27850  opsqrlem5  27853  hmopidmchi  27860  hmopidmpji  27861  pjinvari  27900  pjadj2coi  27913  pj3lem1  27915  funcnvmptOLD  28322  funcnvmpt  28323  pmtrprfv2  28662  madjusmdetlem1  28704  cnre2csqlem  28767  zzsnm  28816  rrhcn  28852  qqhre  28875  oms0  29175  omsmon  29176  omssubaddlem  29177  omssubadd  29178  oms0OLD  29179  omsmonOLD  29180  omssubaddlemOLD  29181  omssubaddOLD  29182  eulerpart  29265  fib0  29282  fib1  29283  fibp1  29284  coinflippv  29366  gsumnunsn  29475  derangenlem  29944  kur14lem2  29980  kur14lem3  29981  kur14lem5  29983  kur14lem6  29984  txsconlem  30013  cvmliftlem4  30061  cvmliftlem5  30062  trpredmintr  30522  trpred0  30527  frrlem5  30568  funpartfv  30762  fullfunfv  30764  neibastop2lem  31066  dffinxpf  31823  ftc1cnnc  32062  heiborlem4  32192  heiborlem6  32194  cdlemk13  34465  cdlemk14  34467  cdlemk15  34468  cdlemk21N  34486  cdlemk20  34487  cdlemk56w  34586  lcfrlem1  35156  hdmapfval  35444  rabdiophlem2  35691  dnnumch1  35948  aomclem6  35963  mncn0  36044  aaitgo  36074  rngunsnply  36085  cytpval  36132  binomcxplemdvsum  36749  binomcxplemnotnn0  36750  binomcxp  36751  fsumsermpt  37743  fmul01  37744  fmuldfeq  37747  fmul01lt1lem1  37748  fmul01lt1lem2  37749  lptioo2cn  37812  lptioo1cn  37813  limclner  37818  dvsinax  37869  fperdvper  37876  dvnmul  37904  dvnprodlem1  37907  dvnprodlem2  37908  dvnprodlem3  37909  itgsin0pilem1  37912  stoweidlem3  37964  stoweidlem17  37978  stoweidlem47  38009  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem62  38133  fourierdlem80  38151  fourierdlem90  38161  fourierdlem92  38163  fourierdlem93  38164  fourierdlem103  38174  fourierdlem104  38175  fouriercnp  38191  sge0isum  38372  sge0seq  38391  ovnsubadd  38501  fpropnf1  39174  ushgredgedga  39452  ushgredgedgaloop  39454  subgruhgredgd  39502  vtxdumgrval  39686  vtxdushgrfvedg  39689  uhgrvd0nedgb  39691  isrgr  39723  fusgrregdegfi  39732  1wlk1walk  39793  11wlkdlem4  39951  1pthond  39955  1wlk2v2elem2  39967  21wlkdlem3  39972  21wlkdlem8  39978  21wlkond  39982  umgr2adedgwlk  39990  31wlkdlem3  39998  31wlkdlem8  40004  3cycld  40015  3cyclpd  40016  rhmsubclem2  40458  rhmsubcALTVlem2  40477  ply1mulgsum  40551  lineval  40555  lincvalpr  40580  lindslinindimp2lem4  40623  zlmodzxzldeplem3  40664  zlmodzxzldeplem4  40665
  Copyright terms: Public domain W3C validator