Theorem fveq1i 5466

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

Syntax hints:   = wceq 1335  ‘cfv 5167

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-uni 3773  df-br 3966  df-iota 5132  df-fv 5175

This theorem is referenced by:  fveq12i  5471  fvun2  5532  fvopab3ig  5539  fvsnun1  5661  fvsnun2  5662  fvpr1  5668  fvpr2  5669  fvpr1g  5670  fvpr2g  5671  fvtp1g  5672  fvtp2g  5673  fvtp3g  5674  fvtp2  5676  fvtp3  5677  ov  5934  ovigg  5935  ovg  5953  tfr2a  6262  tfrex  6309  frec0g  6338  freccllem  6343  frecsuclem  6347  caseinl  7025  caseinr  7026  ctssdccl  7045  addpiord  7219  mulpiord  7220  fseq1p1m1  9978  frec2uz0d  10280  frec2uzzd  10281  frec2uzsucd  10282  frecuzrdgrrn  10289  frec2uzrdg  10290  frecuzrdg0  10294  frecuzrdgsuc  10295  frecuzrdgg  10297  frecuzrdg0t  10303  frecuzrdgsuctlem  10304  0tonninf  10320  1tonninf  10321  inftonninf  10322  seq3val  10339  seqvalcd  10340  hashinfom  10634  hashennn  10636  hashfz1  10639  shftidt  10715  resqrexlemf1  10890  resqrexlemfp1  10891  cbvsum  11239  fisumss  11271  fsumadd  11285  isumclim3  11302  cbvprod  11437  fprodssdc  11469  ialgr0  11901  algrp1  11903  ennnfonelem0  12106  ennnfonelemp1  12107  ennnfonelemom  12109  ctinfomlemom  12128  ndxarg  12173  strslfv2d  12192  upxp  12632  cnmetdval  12889  remetdval  12899  reeflog  13144