Theorem fveq1i 5306

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

Syntax hints:   = wceq 1289   ` cfv 5015

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-uni 3654  df-br 3846  df-iota 4980  df-fv 5023

This theorem is referenced by:  fveq12i  5311  fvun2  5371  fvopab3ig  5378  fvsnun1  5494  fvsnun2  5495  fvpr1  5501  fvpr2  5502  fvpr1g  5503  fvpr2g  5504  fvtp1g  5505  fvtp2g  5506  fvtp3g  5507  fvtp2  5509  fvtp3  5510  ov  5764  ovigg  5765  ovg  5783  tfr2a  6086  tfrex  6133  frec0g  6162  freccllem  6167  frecsuclem  6171  addpiord  6873  mulpiord  6874  fseq1p1m1  9504  frec2uz0d  9802  frec2uzzd  9803  frec2uzsucd  9804  frecuzrdgrrn  9811  frec2uzrdg  9812  frecuzrdg0  9816  frecuzrdgsuc  9817  frecuzrdgg  9819  frecuzrdg0t  9825  frecuzrdgsuctlem  9826  0tonninf  9841  1tonninf  9842  inftonninf  9843  iseqvalt  9869  seq3val  9870  hashinfom  10182  hashennn  10184  hashfz1  10187  shftidt  10263  resqrexlemf1  10437  resqrexlemfp1  10438  cbvsum  10745  fisumss  10780  fsumadd  10796  isumclim3  10813  ialgr0  11300  ialgrp1  11302  ndxarg  11515  strnfv2d  11531