Theorem fveq1i 6832

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

Syntax hints:   = wceq 1541  ‘cfv 6489

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497

This theorem is referenced by:  fveq12i  6837  fvun2  6923  fvopab3ig  6934  fvsnun1  7125  fvpr1g  7133  fvpr2g  7134  fvtp1  7138  fvtp2  7139  fvtp3  7140  fvtp1g  7141  fvtp2g  7142  fvtp3g  7143  fpropnf1  7210  fveqf1o  7245  ov  7499  ovigg  7500  ovg  7520  fvresex  7901  curry1  8043  curry2  8046  fsplitfpar  8057  suppsnop  8117  frrlem12  8236  fprlem1  8239  tfr2a  8323  rdgsucmptf  8356  rdgsucmptnf  8357  frsucmpt  8366  frsucmptn  8367  seqomlem1  8378  seqomlem3  8380  seqomlem4  8381  seqom0g  8384  seqomsuc  8385  unblem2  9188  inf3lemb  9526  inf3lemc  9527  ttrclselem1  9626  ttrclselem2  9627  trcl  9629  frrlem15  9661  r10  9672  r1sucg  9673  r1limg  9675  infxpenc2  9924  aleph0  9968  alephlim  9969  alephsuc  9970  alephfplem1  10006  alephfplem2  10007  ackbij2lem3  10142  cfsmolem  10172  infpssrlem1  10205  infpssrlem2  10206  fin23lem34  10248  fin23lem35  10249  isf32lem6  10260  isf32lem7  10261  isf32lem8  10262  isf34lem5  10280  hsmexlem7  10325  axdclem2  10422  canthp1lem2  10555  wunex2  10640  wuncval2  10649  addpiord  10786  mulpiord  10787  addpqnq  10840  mulpqnq  10843  fseq1p1m1  13505  om2uz0i  13861  om2uzrdg  13870  uzrdg0i  13873  uzrdgsuci  13874  hashkf  14246  hashgval  14247  hashinf  14249  ccat1st1st  14543  revs1  14679  cats1fv  14773  shftidt  14996  cbvsum  15609  cbvsumv  15610  fsumss  15639  isumclim3  15673  isumsup2  15760  cbvprod  15827  cbvprodv  15828  fprodss  15862  iprodclim3  15914  fprodefsum  16009  ruclem4  16150  ruclem6  16151  ruclem7  16152  sadc0  16372  sadcp1  16373  sadcaddlem  16375  sadaddlem  16384  smup0  16397  smupp1  16398  algr0  16490  algrp1  16492  ndxarg  17114  strfv2d  17119  funcoppc  17790  fthepi  17845  homadm  17955  homacd  17956  prdsidlem  18685  prdsinvlem  18970  cayleylem2  19333  symggen  19390  pmtr3ncomlem1  19393  gsumval3  19827  gsumzaddlem  19841  gsumzmhm  19857  pgpfaclem1  20003  ringidval  20109  rhmsubclem2  20610  lidlval  21156  rspval  21157  lidlnegcl  21168  lpival  21270  znf1o  21497  ply1ascl0  22186  ply1ascl1  22187  eqcoe1ply1eq  22234  evls1val  22255  evl1val  22264  mat1dimmul  22411  mdetralt  22543  mdetunilem7  22553  decpmatid  22705  pmatcollpwscmatlem1  22724  cpmidpmat  22808  chcoeffeq  22821  restcls  23116  restntr  23117  upxp  23558  cnmetdval  24705  remetdval  24724  qdensere2  24732  pcoptcl  24968  pcopt  24969  pcopt2  24970  pcorevlem  24973  isncvsngp  25096  cnncvsabsnegdemo  25112  ovolfsval  25418  ovollb2lem  25436  ovolunlem1a  25444  ovoliunlem1  25450  ovoliun2  25454  ovolscalem1  25461  ovolicc2lem4  25468  mblvol  25478  ioombl1lem4  25509  uniioovol  25527  uniioombllem3  25533  0pval  25619  limccnp  25839  limccnp2  25840  dvcnvrelem2  25970  itgsubstlem  26002  ply1remlem  26117  plyrem  26260  qaa  26278  abelth  26398  efif1olem4  26501  eflog  26532  logef  26537  logeftb  26539  dvrelog  26593  dvlog  26607  cxpcn3  26705  efrlim  26926  efrlimOLD  26927  eflgam  27002  wilthlem3  27027  basellem8  27045  lgsqrlem1  27304  noetasuplem4  27695  noetainflem4  27699  precsexlem1  28165  precsexlem2  28166  precsexlem3  28167  precsexlem4  28168  precsexlem5  28169  tgcgr4  28529  krippenlem  28688  colperpexlem1  28728  opphllem3  28747  lmiisolem  28794  axlowdimlem8  28948  axlowdimlem9  28949  axlowdimlem11  28951  axlowdimlem12  28952  axlowdimlem17  28957  ushgredgedg  29228  ushgredgedgloop  29230  subgruhgredgd  29283  vtxdlfgrval  29485  vtxd0nedgb  29488  vtxdushgrfvedg  29490  vtxdginducedm1lem3  29541  finsumvtxdg2size  29550  vtxdgoddnumeven  29553  isrgr  29559  fusgrregdegfi  29569  wlk1walk  29638  wlkres  29668  wlkp1lem5  29675  wlkp1lem6  29676  wlkp1lem7  29677  wlkp1lem8  29678  clwlkcompbp  29781  crctcshwlkn0lem4  29812  crctcshwlkn0lem5  29813  crctcshwlkn0lem6  29814  2wlkdlem3  29926  2wlkdlem8  29932  2wlkond  29936  umgr2adedgwlk  29944  1wlkdlem4  30141  1pthond  30145  wlk2v2elem2  30157  3wlkdlem3  30162  3wlkdlem8  30168  3cycld  30179  3cyclpd  30180  eucrctshift  30244  frgrncvvdeq  30310  frgrwopreglem2  30314  ex-fpar  30463  avril1  30464  vafval  30604  smfval  30606  0vfval  30607  nmcvfval  30608  vsfval  30634  hhssabloilem  31262  pjoc2i  31439  pjcji  31685  ho0val  31751  hoival  31756  adjbdlnb  32085  nmopcoadji  32102  opsqrlem2  32142  opsqrlem5  32145  hmopidmchi  32152  hmopidmpji  32153  pjinvari  32192  pjadj2coi  32205  pj3lem1  32207  funcnvmpt  32671  pmtrprfv2  33098  cycpmco2lem7  33142  evl1fpws  33573  mplmulmvr  33632  evlextv  33635  esplyind  33659  esplyindfv  33660  esplyfvn  33661  vietalem  33663  rgmoddimOLD  33695  rtelextdg2lem  33811  constr0  33822  constrsuc  33823  constrlim  33824  2sqr3minply  33865  cos9thpiminplylem6  33872  madjusmdetlem1  33912  cnre2csqlem  33995  zzsnm  34044  rrhcn  34082  qqhre  34105  oms0  34382  omsmon  34383  omssubaddlem  34384  omssubadd  34385  eulerpart  34467  fib0  34484  fib1  34485  fibp1  34486  coinflippv  34569  gsumnunsn  34626  2cycld  35254  derangenlem  35287  kur14lem2  35323  kur14lem3  35324  kur14lem5  35326  kur14lem6  35327  txsconnlem  35356  cvmliftlem4  35404  cvmliftlem5  35405  satf0sucom  35489  satf0suc  35492  satf0op  35493  fmla  35497  satffunlem2lem2  35522  satfv0fvfmla0  35529  sate0  35531  funpartfv  36061  fullfunfv  36063  sumeq2si  36318  prodeq2si  36320  cbvprodvw2  36363  neibastop2lem  36476  dffinxpf  37502  ftc1cnnc  37805  heiborlem4  37927  heiborlem6  37929  cdlemk13  41024  cdlemk14  41026  cdlemk15  41027  cdlemk21N  41045  cdlemk20  41046  cdlemk56w  41145  lcfrlem1  41714  hdmapfval  41999  deg1gprod  42306  evlsevl  42732  selvvvval  42743  rabdiophlem2  42959  dnnumch1  43201  aomclem6  43216  mncn0  43296  aaitgo  43319  rngunsnply  43326  cytpval  43359  dssmapntrcls  44285  binomcxplemdvsum  44512  binomcxplemnotnn0  44513  binomcxp  44514  fvcod  45387  fvmpt2df  45432  fsumsermpt  45741  fmul01  45742  fmuldfeq  45745  fmul01lt1lem1  45746  fmul01lt1lem2  45747  lptioo2cn  45805  lptioo1cn  45806  limclner  45811  dvsinax  46073  fperdvper  46079  dvnmul  46103  dvnprodlem1  46106  dvnprodlem2  46107  dvnprodlem3  46108  itgsin0pilem1  46110  stoweidlem3  46163  stoweidlem17  46177  stoweidlem47  46207  fourierdlem42  46309  fourierdlem62  46328  fourierdlem80  46346  fourierdlem90  46356  fourierdlem92  46358  fourierdlem93  46359  fourierdlem103  46369  fourierdlem104  46370  fouriercnp  46386  sge0isum  46587  sge0seq  46606  ovnsubadd  46732  vonn0ioo  46847  vonn0icc  46848  smflimsup  46988  cjnpoly  47051  sinnpoly  47053  fcores  47229  fundcmpsurinjimaid  47573  isgrim  48044  gricushgr  48079  gpgprismgr4cycllem3  48259  gpgprismgr4cycllem6  48262  gpgprismgr4cycllem7  48263  gpgprismgr4cycllem10  48266  rhmsubcALTVlem2  48444  ply1mulgsum  48552  lineval  48556  lincvalpr  48580  lindslinindimp2lem4  48623  zlmodzxzldeplem3  48664  zlmodzxzldeplem4  48665  itcoval0mpt  48828  ackvalsuc1mpt  48840  ackval0  48842  ackval40  48855  ackval41a  48856  ackval42  48858  ackval50  48860  ehl2eudisval0  48887  2sphere0  48912  line2  48914  line2x  48916  line2y  48917  itscnhlinecirc02p  48947  oppcup  49368  natoppf  49390