Theorem fveq1i 6192

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
fveq1i	⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		fveq1 6190	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Syntax hints:   = wceq 1483  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896

This theorem is referenced by:  fveq12i  6196  fvun2  6270  fvopab3ig  6278  fvsnun1  6448  fvsnun2  6449  fvpr1  6456  fvpr2  6457  fvpr1g  6458  fvpr2g  6459  fvtp1  6460  fvtp2  6461  fvtp3  6462  fvtp1g  6463  fvtp2g  6464  fvtp3g  6465  fpropnf1  6524  fveqf1o  6557  ov  6780  ovigg  6781  ovg  6799  fvresex  7139  curry1  7269  curry2  7272  suppsnop  7309  wfrlem5  7419  tfr2a  7491  rdgsucmptf  7524  rdgsucmptnf  7525  frsucmpt  7533  frsucmptn  7534  seqomlem1  7545  seqomlem3  7547  seqomlem4  7548  seqom0g  7551  seqomsuc  7552  unblem2  8213  inf3lemb  8522  inf3lemc  8523  trcl  8604  r10  8631  r1sucg  8632  r1limg  8634  infxpenc2  8845  aleph0  8889  alephlim  8890  alephsuc  8891  alephfplem1  8927  alephfplem2  8928  ackbij2lem3  9063  cfsmolem  9092  infpssrlem1  9125  infpssrlem2  9126  fin23lem34  9168  fin23lem35  9169  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  isf34lem5  9200  hsmexlem7  9245  axdclem2  9342  canthp1lem2  9475  wunex2  9560  wuncval2  9569  addpiord  9706  mulpiord  9707  addpqnq  9760  mulpqnq  9763  fseq1p1m1  12414  om2uz0i  12746  om2uzrdg  12755  uzrdg0i  12758  uzrdgsuci  12759  hashkf  13119  hashgval  13120  hashinf  13122  revs1  13514  cats1fv  13604  shftidt  13822  cbvsum  14425  fsumss  14456  isumclim3  14490  isumsup2  14578  cbvprod  14645  fprodss  14678  iprodclim3  14731  fprodefsum  14825  ruclem4  14963  ruclem6  14964  ruclem7  14965  sadc0  15176  sadcp1  15177  sadcaddlem  15179  sadaddlem  15188  smup0  15201  smupp1  15202  algr0  15285  algrp1  15287  ndxarg  15882  strfv2d  15905  xpsc0  16220  xpsc1  16221  funcoppc  16535  fthepi  16588  homadm  16690  homacd  16691  prdsidlem  17322  prdsinvlem  17524  cayleylem2  17833  symggen  17890  pmtr3ncomlem1  17893  gsumval3  18308  gsumzaddlem  18321  gsumzmhm  18337  pgpfaclem1  18480  ringidval  18503  lidlval  19192  rspval  19193  lidlnegcl  19214  lpival  19245  eqcoe1ply1eq  19667  evls1val  19685  evl1val  19693  znf1o  19900  mat1dimmul  20282  mdetralt  20414  mdetunilem7  20424  decpmatid  20575  pmatcollpwscmatlem1  20594  cpmidpmat  20678  chcoeffeq  20691  restcls  20985  restntr  20986  upxp  21426  cnmetdval  22574  remetdval  22592  qdensere2  22600  pcoptcl  22821  pcopt  22822  pcopt2  22823  pcorevlem  22826  isncvsngp  22949  cnncvsabsnegdemo  22965  ovolfsval  23239  ovollb2lem  23256  ovolunlem1a  23264  ovoliunlem1  23270  ovoliun2  23274  ovolscalem1  23281  ovolicc2lem4  23288  mblvol  23298  ioombl1lem4  23329  uniioovol  23347  uniioombllem3  23353  0pval  23438  limccnp  23655  limccnp2  23656  dvcnvrelem2  23781  itgsubstlem  23811  ply1remlem  23922  plyrem  24060  qaa  24078  abelth  24195  efif1olem4  24291  eflog  24323  logef  24328  logeftb  24330  dvrelog  24383  dvlog  24397  cxpcn3  24489  efrlim  24696  eflgam  24771  wilthlem3  24796  basellem8  24814  lgsqrlem1  25071  tgcgr4  25426  krippenlem  25585  colperpexlem1  25622  opphllem3  25641  lmiisolem  25688  axlowdimlem8  25829  axlowdimlem9  25830  axlowdimlem11  25832  axlowdimlem12  25833  axlowdimlem17  25838  ushgredgedg  26121  ushgredgedgloop  26123  subgruhgredgd  26176  vtxdlfgrval  26381  vtxd0nedgb  26384  vtxdushgrfvedg  26386  vtxdginducedm1lem3  26437  finsumvtxdg2size  26446  vtxdgoddnumeven  26449  isrgr  26455  fusgrregdegfi  26465  wlk1walk  26535  wlkres  26567  wlkp1lem5  26574  wlkp1lem6  26575  wlkp1lem7  26576  wlkp1lem8  26577  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  wlkwwlksur  26783  2wlkdlem3  26823  2wlkdlem8  26829  2wlkond  26833  umgr2adedgwlk  26841  1wlkdlem4  27000  1pthond  27004  wlk2v2elem2  27016  3wlkdlem3  27021  3wlkdlem8  27027  3cycld  27038  3cyclpd  27039  eucrctshift  27103  frgrncvvdeq  27173  frgrwopreglem2  27177  avril1  27319  vafval  27458  smfval  27460  0vfval  27461  nmcvfval  27462  vsfval  27488  hhssabloilem  28118  pjoc2i  28297  pjcji  28543  ho0val  28609  hoival  28614  adjbdlnb  28943  nmopcoadji  28960  opsqrlem2  29000  opsqrlem5  29003  hmopidmchi  29010  hmopidmpji  29011  pjinvari  29050  pjadj2coi  29063  pj3lem1  29065  funcnvmptOLD  29467  funcnvmpt  29468  pmtrprfv2  29848  madjusmdetlem1  29893  cnre2csqlem  29956  zzsnm  30005  rrhcn  30041  qqhre  30064  oms0  30359  omsmon  30360  omssubaddlem  30361  omssubadd  30362  eulerpart  30444  fib0  30461  fib1  30462  fibp1  30463  coinflippv  30545  gsumnunsn  30615  derangenlem  31153  kur14lem2  31189  kur14lem3  31190  kur14lem5  31192  kur14lem6  31193  txsconnlem  31222  cvmliftlem4  31270  cvmliftlem5  31271  trpredmintr  31731  trpred0  31736  frrlem5  31784  noetalem3  31865  funpartfv  32052  fullfunfv  32054  neibastop2lem  32355  dffinxpf  33222  ftc1cnnc  33484  heiborlem4  33613  heiborlem6  33615  cdlemk13  36140  cdlemk14  36142  cdlemk15  36143  cdlemk21N  36161  cdlemk20  36162  cdlemk56w  36261  lcfrlem1  36831  hdmapfval  37119  rabdiophlem2  37366  dnnumch1  37614  aomclem6  37629  mncn0  37709  aaitgo  37732  rngunsnply  37743  cytpval  37787  dssmapntrcls  38426  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  binomcxp  38556  fvcod  39423  fsumsermpt  39811  fmul01  39812  fmuldfeq  39815  fmul01lt1lem1  39816  fmul01lt1lem2  39817  lptioo2cn  39877  lptioo1cn  39878  limclner  39883  dvsinax  40127  fperdvper  40133  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  itgsin0pilem1  40165  stoweidlem3  40220  stoweidlem17  40234  stoweidlem47  40264  fourierdlem42  40366  fourierdlem62  40385  fourierdlem80  40403  fourierdlem90  40413  fourierdlem92  40415  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fouriercnp  40443  sge0isum  40644  sge0seq  40663  ovnsubadd  40786  vonn0ioo  40901  vonn0icc  40902  smflimsup  41034  rhmsubclem2  42087  rhmsubcALTVlem2  42105  ply1mulgsum  42178  lineval  42182  lincvalpr  42207  lindslinindimp2lem4  42250  zlmodzxzldeplem3  42291  zlmodzxzldeplem4  42292