Theorem fveq1i 5556

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1i.1	|- F = G

Assertion

Ref	Expression
fveq1i	|- ( F ` A ) = ( G ` A )

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 |- F = G
2		fveq1 5554	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	ax-mp 5	1 |- ( F ` A ) = ( G ` A )

Syntax hints:   = wceq 1364   ` cfv 5255

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263

This theorem is referenced by:  fveq12i  5561  fvun2  5625  fvopab3ig  5632  fvsnun1  5756  fvsnun2  5757  fvpr1  5763  fvpr2  5764  fvpr1g  5765  fvpr2g  5766  fvtp1g  5767  fvtp2g  5768  fvtp3g  5769  fvtp2  5771  fvtp3  5772  ov  6039  ovigg  6040  ovg  6059  tfr2a  6376  tfrex  6423  frec0g  6452  freccllem  6457  frecsuclem  6461  caseinl  7152  caseinr  7153  ctssdccl  7172  addpiord  7378  mulpiord  7379  fseq1p1m1  10163  frec2uz0d  10473  frec2uzzd  10474  frec2uzsucd  10475  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdg0  10487  frecuzrdgsuc  10488  frecuzrdgg  10490  frecuzrdg0t  10496  frecuzrdgsuctlem  10497  0tonninf  10514  1tonninf  10515  inftonninf  10516  seq3val  10534  seqvalcd  10535  hashinfom  10852  hashennn  10854  hashfz1  10857  shftidt  10980  resqrexlemf1  11155  resqrexlemfp1  11156  cbvsum  11506  fisumss  11538  fsumadd  11552  isumclim3  11569  cbvprod  11704  fprodssdc  11736  nninfctlemfo  12180  ialgr0  12185  algrp1  12187  ennnfonelem0  12565  ennnfonelemp1  12566  ennnfonelemom  12568  ctinfomlemom  12587  nninfdclemp1  12610  ndxarg  12644  strslfv2d  12664  ringidvalg  13460  lidlvalg  13970  rspvalg  13971  znf1o  14150  upxp  14451  cnmetdval  14708  remetdval  14726  reeflog  15039