Theorem fveq1i 5555

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 5553	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	ax-mp 5	1 |- ( F ` A ) = ( G ` A )

Syntax hints:   = wceq 1364   ` cfv 5254

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 3836  df-br 4030  df-iota 5215  df-fv 5262

This theorem is referenced by:  fveq12i  5560  fvun2  5624  fvopab3ig  5631  fvsnun1  5755  fvsnun2  5756  fvpr1  5762  fvpr2  5763  fvpr1g  5764  fvpr2g  5765  fvtp1g  5766  fvtp2g  5767  fvtp3g  5768  fvtp2  5770  fvtp3  5771  ov  6038  ovigg  6039  ovg  6057  tfr2a  6374  tfrex  6421  frec0g  6450  freccllem  6455  frecsuclem  6459  caseinl  7150  caseinr  7151  ctssdccl  7170  addpiord  7376  mulpiord  7377  fseq1p1m1  10160  frec2uz0d  10470  frec2uzzd  10471  frec2uzsucd  10472  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdg0  10484  frecuzrdgsuc  10485  frecuzrdgg  10487  frecuzrdg0t  10493  frecuzrdgsuctlem  10494  0tonninf  10511  1tonninf  10512  inftonninf  10513  seq3val  10531  seqvalcd  10532  hashinfom  10849  hashennn  10851  hashfz1  10854  shftidt  10977  resqrexlemf1  11152  resqrexlemfp1  11153  cbvsum  11503  fisumss  11535  fsumadd  11549  isumclim3  11566  cbvprod  11701  fprodssdc  11733  nninfctlemfo  12177  ialgr0  12182  algrp1  12184  ennnfonelem0  12562  ennnfonelemp1  12563  ennnfonelemom  12565  ctinfomlemom  12584  nninfdclemp1  12607  ndxarg  12641  strslfv2d  12661  ringidvalg  13457  lidlvalg  13967  rspvalg  13968  znf1o  14139  upxp  14440  cnmetdval  14697  remetdval  14707  reeflog  14998