Theorem fveq1i 5671

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

Syntax hints:   = wceq 1398  ‘cfv 5352

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360

This theorem is referenced by:  fveq12i  5676  fvun2  5744  fvopab3ig  5751  fvsnun1  5881  fvsnun2  5882  fvpr1  5888  fvpr2  5889  fvpr1g  5890  fvpr2g  5891  fvtp1g  5892  fvtp2g  5893  fvtp3g  5894  fvtp2  5896  fvtp3  5897  ov  6173  ovigg  6174  ovg  6193  suppsnopdc  6450  tfr2a  6552  tfrex  6599  frec0g  6628  freccllem  6633  frecsuclem  6637  caseinl  7382  caseinr  7383  ctssdccl  7402  addpiord  7631  mulpiord  7632  fseq1p1m1  10428  frec2uz0d  10761  frec2uzzd  10762  frec2uzsucd  10763  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdg0  10775  frecuzrdgsuc  10776  frecuzrdgg  10778  frecuzrdg0t  10784  frecuzrdgsuctlem  10785  0tonninf  10802  1tonninf  10803  inftonninf  10804  seq3val  10822  seqvalcd  10823  hashinfom  11141  hashennn  11143  hashfz1  11146  ccat1st1st  11329  cats1fvd  11458  shftidt  11518  resqrexlemf1  11693  resqrexlemfp1  11694  cbvsum  12045  fisumss  12078  fsumadd  12092  isumclim3  12109  cbvprod  12244  fprodssdc  12276  nninfctlemfo  12736  ialgr0  12741  algrp1  12743  ennnfonelem0  13156  ennnfonelemp1  13157  ennnfonelemom  13159  ctinfomlemom  13178  nninfdclemp1  13201  ndxarg  13235  strslfv2d  13255  prdsidlem  13660  prdsinvlem  13821  ringidvalg  14105  lidlvalg  14619  rspvalg  14620  znf1o  14799  mplnegfi  14860  upxp  15137  cnmetdval  15394  remetdval  15412  reeflog  15728  ushgredgedg  16221  ushgredgedgloop  16223  subgruhgredgdm  16265  vtxdumgrfival  16293  vtxd0nedgbfi  16294  vtxduspgrfvedgfi  16296  wlk1walkdom  16354  wlkres  16374  depindlem1  16501  nninfnfiinf  16801