Theorem fveq1i 6671

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 6669	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Syntax hints:   = wceq 1537  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  fveq12i  6676  fvun2  6755  fvopab3ig  6764  fvsnun1  6944  fvpr1  6952  fvpr2  6953  fvpr1g  6954  fvpr2g  6955  fvtp1  6957  fvtp2  6958  fvtp3  6959  fvtp1g  6960  fvtp2g  6961  fvtp3g  6962  fpropnf1  7025  fveqf1o  7058  ov  7294  ovigg  7295  ovg  7313  fvresex  7661  curry1  7799  curry2  7802  fsplitfpar  7814  suppsnop  7844  wfrlem5  7959  tfr2a  8031  rdgsucmptf  8064  rdgsucmptnf  8065  frsucmpt  8073  frsucmptn  8074  seqomlem1  8086  seqomlem3  8088  seqomlem4  8089  seqom0g  8092  seqomsuc  8093  unblem2  8771  inf3lemb  9088  inf3lemc  9089  trcl  9170  r10  9197  r1sucg  9198  r1limg  9200  infxpenc2  9448  aleph0  9492  alephlim  9493  alephsuc  9494  alephfplem1  9530  alephfplem2  9531  ackbij2lem3  9663  cfsmolem  9692  infpssrlem1  9725  infpssrlem2  9726  fin23lem34  9768  fin23lem35  9769  isf32lem6  9780  isf32lem7  9781  isf32lem8  9782  isf34lem5  9800  hsmexlem7  9845  axdclem2  9942  canthp1lem2  10075  wunex2  10160  wuncval2  10169  addpiord  10306  mulpiord  10307  addpqnq  10360  mulpqnq  10363  fseq1p1m1  12982  om2uz0i  13316  om2uzrdg  13325  uzrdg0i  13328  uzrdgsuci  13329  hashkf  13693  hashgval  13694  hashinf  13696  ccat1st1st  13984  revs1  14127  cats1fv  14221  shftidt  14441  cbvsum  15052  fsumss  15082  isumclim3  15114  isumsup2  15201  cbvprod  15269  fprodss  15302  iprodclim3  15354  fprodefsum  15448  ruclem4  15587  ruclem6  15588  ruclem7  15589  sadc0  15803  sadcp1  15804  sadcaddlem  15806  sadaddlem  15815  smup0  15828  smupp1  15829  algr0  15916  algrp1  15918  ndxarg  16508  strfv2d  16529  funcoppc  17145  fthepi  17198  homadm  17300  homacd  17301  prdsidlem  17943  prdsinvlem  18208  cayleylem2  18541  symggen  18598  pmtr3ncomlem1  18601  gsumval3  19027  gsumzaddlem  19041  gsumzmhm  19057  pgpfaclem1  19203  ringidval  19253  lidlval  19964  rspval  19965  lidlnegcl  19987  lpival  20018  eqcoe1ply1eq  20465  evls1val  20483  evl1val  20492  znf1o  20698  mat1dimmul  21085  mdetralt  21217  mdetunilem7  21227  decpmatid  21378  pmatcollpwscmatlem1  21397  cpmidpmat  21481  chcoeffeq  21494  restcls  21789  restntr  21790  upxp  22231  cnmetdval  23379  remetdval  23397  qdensere2  23405  pcoptcl  23625  pcopt  23626  pcopt2  23627  pcorevlem  23630  isncvsngp  23753  cnncvsabsnegdemo  23769  ovolfsval  24071  ovollb2lem  24089  ovolunlem1a  24097  ovoliunlem1  24103  ovoliun2  24107  ovolscalem1  24114  ovolicc2lem4  24121  mblvol  24131  ioombl1lem4  24162  uniioovol  24180  uniioombllem3  24186  0pval  24272  limccnp  24489  limccnp2  24490  dvcnvrelem2  24615  itgsubstlem  24645  ply1remlem  24756  plyrem  24894  qaa  24912  abelth  25029  efif1olem4  25129  eflog  25160  logef  25165  logeftb  25167  dvrelog  25220  dvlog  25234  cxpcn3  25329  efrlim  25547  eflgam  25622  wilthlem3  25647  basellem8  25665  lgsqrlem1  25922  tgcgr4  26317  krippenlem  26476  colperpexlem1  26516  opphllem3  26535  lmiisolem  26582  axlowdimlem8  26735  axlowdimlem9  26736  axlowdimlem11  26738  axlowdimlem12  26739  axlowdimlem17  26744  ushgredgedg  27011  ushgredgedgloop  27013  subgruhgredgd  27066  vtxdlfgrval  27267  vtxd0nedgb  27270  vtxdushgrfvedg  27272  vtxdginducedm1lem3  27323  finsumvtxdg2size  27332  vtxdgoddnumeven  27335  isrgr  27341  fusgrregdegfi  27351  wlk1walk  27420  wlkres  27452  wlkp1lem5  27459  wlkp1lem6  27460  wlkp1lem7  27461  wlkp1lem8  27462  clwlkcompbp  27563  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  2wlkdlem3  27706  2wlkdlem8  27712  2wlkond  27716  umgr2adedgwlk  27724  1wlkdlem4  27919  1pthond  27923  wlk2v2elem2  27935  3wlkdlem3  27940  3wlkdlem8  27946  3cycld  27957  3cyclpd  27958  eucrctshift  28022  frgrncvvdeq  28088  frgrwopreglem2  28092  ex-fpar  28241  avril1  28242  vafval  28380  smfval  28382  0vfval  28383  nmcvfval  28384  vsfval  28410  hhssabloilem  29038  pjoc2i  29215  pjcji  29461  ho0val  29527  hoival  29532  adjbdlnb  29861  nmopcoadji  29878  opsqrlem2  29918  opsqrlem5  29921  hmopidmchi  29928  hmopidmpji  29929  pjinvari  29968  pjadj2coi  29981  pj3lem1  29983  funcnvmpt  30412  pmtrprfv2  30732  cycpmco2lem7  30774  rgmoddim  31008  madjusmdetlem1  31092  cnre2csqlem  31153  zzsnm  31202  rrhcn  31238  qqhre  31261  oms0  31555  omsmon  31556  omssubaddlem  31557  omssubadd  31558  eulerpart  31640  fib0  31657  fib1  31658  fibp1  31659  coinflippv  31741  gsumnunsn  31811  2cycld  32385  derangenlem  32418  kur14lem2  32454  kur14lem3  32455  kur14lem5  32457  kur14lem6  32458  txsconnlem  32487  cvmliftlem4  32535  cvmliftlem5  32536  satf0sucom  32620  satf0suc  32623  satf0op  32624  fmla  32628  satffunlem2lem2  32653  satfv0fvfmla0  32660  sate0  32662  trpredmintr  33070  trpred0  33075  frrlem12  33134  fprlem1  33137  frrlem15  33142  noetalem3  33219  funpartfv  33406  fullfunfv  33408  neibastop2lem  33708  dffinxpf  34669  ftc1cnnc  34981  heiborlem4  35107  heiborlem6  35109  cdlemk13  38003  cdlemk14  38005  cdlemk15  38006  cdlemk21N  38024  cdlemk20  38025  cdlemk56w  38124  lcfrlem1  38693  hdmapfval  38978  rabdiophlem2  39448  dnnumch1  39693  aomclem6  39708  mncn0  39788  aaitgo  39811  rngunsnply  39822  cytpval  39858  dssmapntrcls  40527  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  binomcxp  40738  fvcod  41541  fsumsermpt  41909  fmul01  41910  fmuldfeq  41913  fmul01lt1lem1  41914  fmul01lt1lem2  41915  lptioo2cn  41975  lptioo1cn  41976  limclner  41981  dvsinax  42246  fperdvper  42252  dvnmul  42277  dvnprodlem1  42280  dvnprodlem2  42281  dvnprodlem3  42282  itgsin0pilem1  42284  stoweidlem3  42337  stoweidlem17  42351  stoweidlem47  42381  fourierdlem42  42483  fourierdlem62  42502  fourierdlem80  42520  fourierdlem90  42530  fourierdlem92  42532  fourierdlem93  42533  fourierdlem103  42543  fourierdlem104  42544  fouriercnp  42560  sge0isum  42758  sge0seq  42777  ovnsubadd  42903  vonn0ioo  43018  vonn0icc  43019  smflimsup  43151  fundcmpsurinjimaid  43620  isomushgr  44040  rhmsubclem2  44407  rhmsubcALTVlem2  44425  ply1mulgsum  44493  lineval  44497  lincvalpr  44522  lindslinindimp2lem4  44565  zlmodzxzldeplem3  44606  zlmodzxzldeplem4  44607  ehl2eudisval0  44761  2sphere0  44786  line2  44788  line2x  44790  line2y  44791  itscnhlinecirc02p  44821