Theorem fveq1i 5676

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

Syntax hints:   = wceq 1398  ‘cfv 5357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  fveq12i  5681  fvun2  5749  fvopab3ig  5756  fvsnun1  5886  fvsnun2  5887  fvpr1  5893  fvpr2  5894  fvpr1g  5895  fvpr2g  5896  fvtp1g  5897  fvtp2g  5898  fvtp3g  5899  fvtp2  5901  fvtp3  5902  ov  6181  ovigg  6182  ovg  6201  suppsnopdc  6463  tfr2a  6565  tfrex  6612  frec0g  6641  freccllem  6646  frecsuclem  6650  caseinl  7395  caseinr  7396  ctssdccl  7415  addpiord  7647  mulpiord  7648  fseq1p1m1  10450  frec2uz0d  10785  frec2uzzd  10786  frec2uzsucd  10787  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdg0  10799  frecuzrdgsuc  10800  frecuzrdgg  10802  frecuzrdg0t  10808  frecuzrdgsuctlem  10809  0tonninf  10826  1tonninf  10827  inftonninf  10828  seq3val  10846  seqvalcd  10847  hashinfom  11166  hashennn  11168  hashfz1  11171  ccat1st1st  11354  cats1fvd  11483  shftidt  11543  resqrexlemf1  11718  resqrexlemfp1  11719  cbvsum  12070  fisumss  12103  fsumadd  12117  isumclim3  12134  cbvprod  12269  fprodssdc  12301  nninfctlemfo  12761  ialgr0  12766  algrp1  12768  ennnfonelem0  13240  ennnfonelemp1  13241  ennnfonelemom  13243  ctinfomlemom  13262  nninfdclemp1  13285  ndxarg  13319  strslfv2d  13339  prdsidlem  14135  prdsinvlem  14138  ringidvalg  14204  lidlvalg  14745  rspvalg  14746  znf1o  14925  mplnegfi  14986  upxp  15263  cnmetdval  15520  remetdval  15538  reeflog  15854  ushgredgedg  16347  ushgredgedgloop  16349  subgruhgredgdm  16391  vtxdumgrfival  16419  vtxd0nedgbfi  16420  vtxduspgrfvedgfi  16422  wlk1walkdom  16480  wlkres  16500  depindlem1  16627  nninfnfiinf  16927