Theorem fveq1i 5577

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

Syntax hints:   = wceq 1373   ` cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279

This theorem is referenced by:  fveq12i  5582  fvun2  5646  fvopab3ig  5653  fvsnun1  5781  fvsnun2  5782  fvpr1  5788  fvpr2  5789  fvpr1g  5790  fvpr2g  5791  fvtp1g  5792  fvtp2g  5793  fvtp3g  5794  fvtp2  5796  fvtp3  5797  ov  6065  ovigg  6066  ovg  6085  tfr2a  6407  tfrex  6454  frec0g  6483  freccllem  6488  frecsuclem  6492  caseinl  7193  caseinr  7194  ctssdccl  7213  addpiord  7429  mulpiord  7430  fseq1p1m1  10216  frec2uz0d  10544  frec2uzzd  10545  frec2uzsucd  10546  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdg0  10558  frecuzrdgsuc  10559  frecuzrdgg  10561  frecuzrdg0t  10567  frecuzrdgsuctlem  10568  0tonninf  10585  1tonninf  10586  inftonninf  10587  seq3val  10605  seqvalcd  10606  hashinfom  10923  hashennn  10925  hashfz1  10928  ccat1st1st  11093  shftidt  11144  resqrexlemf1  11319  resqrexlemfp1  11320  cbvsum  11671  fisumss  11703  fsumadd  11717  isumclim3  11734  cbvprod  11869  fprodssdc  11901  nninfctlemfo  12361  ialgr0  12366  algrp1  12368  ennnfonelem0  12776  ennnfonelemp1  12777  ennnfonelemom  12779  ctinfomlemom  12798  nninfdclemp1  12821  ndxarg  12855  strslfv2d  12875  prdsidlem  13279  prdsinvlem  13440  ringidvalg  13723  lidlvalg  14233  rspvalg  14234  znf1o  14413  mplnegfi  14467  upxp  14744  cnmetdval  15001  remetdval  15019  reeflog  15335  nninfnfiinf  15960