Theorem fveq1i 5430

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

Syntax hints:   = wceq 1332  ‘cfv 5131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139

This theorem is referenced by:  fveq12i  5435  fvun2  5496  fvopab3ig  5503  fvsnun1  5625  fvsnun2  5626  fvpr1  5632  fvpr2  5633  fvpr1g  5634  fvpr2g  5635  fvtp1g  5636  fvtp2g  5637  fvtp3g  5638  fvtp2  5640  fvtp3  5641  ov  5898  ovigg  5899  ovg  5917  tfr2a  6226  tfrex  6273  frec0g  6302  freccllem  6307  frecsuclem  6311  caseinl  6984  caseinr  6985  ctssdccl  7004  addpiord  7148  mulpiord  7149  fseq1p1m1  9905  frec2uz0d  10203  frec2uzzd  10204  frec2uzsucd  10205  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdg0  10217  frecuzrdgsuc  10218  frecuzrdgg  10220  frecuzrdg0t  10226  frecuzrdgsuctlem  10227  0tonninf  10243  1tonninf  10244  inftonninf  10245  seq3val  10262  seqvalcd  10263  hashinfom  10556  hashennn  10558  hashfz1  10561  shftidt  10637  resqrexlemf1  10812  resqrexlemfp1  10813  cbvsum  11161  fisumss  11193  fsumadd  11207  isumclim3  11224  cbvprod  11359  ialgr0  11761  algrp1  11763  ennnfonelem0  11954  ennnfonelemp1  11955  ennnfonelemom  11957  ctinfomlemom  11976  ndxarg  12021  strslfv2d  12040  upxp  12480  cnmetdval  12737  remetdval  12747  reeflog  12992