Theorem fveq1i 5628

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

Syntax hints:   = wceq 1395   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  fveq12i  5633  fvun2  5701  fvopab3ig  5708  fvsnun1  5836  fvsnun2  5837  fvpr1  5843  fvpr2  5844  fvpr1g  5845  fvpr2g  5846  fvtp1g  5847  fvtp2g  5848  fvtp3g  5849  fvtp2  5851  fvtp3  5852  ov  6124  ovigg  6125  ovg  6144  tfr2a  6467  tfrex  6514  frec0g  6543  freccllem  6548  frecsuclem  6552  caseinl  7258  caseinr  7259  ctssdccl  7278  addpiord  7503  mulpiord  7504  fseq1p1m1  10290  frec2uz0d  10621  frec2uzzd  10622  frec2uzsucd  10623  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdg0  10635  frecuzrdgsuc  10636  frecuzrdgg  10638  frecuzrdg0t  10644  frecuzrdgsuctlem  10645  0tonninf  10662  1tonninf  10663  inftonninf  10664  seq3val  10682  seqvalcd  10683  hashinfom  11000  hashennn  11002  hashfz1  11005  ccat1st1st  11172  cats1fvd  11298  shftidt  11344  resqrexlemf1  11519  resqrexlemfp1  11520  cbvsum  11871  fisumss  11903  fsumadd  11917  isumclim3  11934  cbvprod  12069  fprodssdc  12101  nninfctlemfo  12561  ialgr0  12566  algrp1  12568  ennnfonelem0  12976  ennnfonelemp1  12977  ennnfonelemom  12979  ctinfomlemom  12998  nninfdclemp1  13021  ndxarg  13055  strslfv2d  13075  prdsidlem  13480  prdsinvlem  13641  ringidvalg  13924  lidlvalg  14435  rspvalg  14436  znf1o  14615  mplnegfi  14669  upxp  14946  cnmetdval  15203  remetdval  15221  reeflog  15537  ushgredgedg  16024  ushgredgedgloop  16026  wlk1walkdom  16070  nninfnfiinf  16389