Theorem fveq1i 5649

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

Syntax hints:   = wceq 1398   ` cfv 5333

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  fveq12i  5654  fvun2  5722  fvopab3ig  5729  fvsnun1  5859  fvsnun2  5860  fvpr1  5866  fvpr2  5867  fvpr1g  5868  fvpr2g  5869  fvtp1g  5870  fvtp2g  5871  fvtp3g  5872  fvtp2  5874  fvtp3  5875  ov  6151  ovigg  6152  ovg  6171  suppsnopdc  6428  tfr2a  6530  tfrex  6577  frec0g  6606  freccllem  6611  frecsuclem  6615  caseinl  7350  caseinr  7351  ctssdccl  7370  addpiord  7596  mulpiord  7597  fseq1p1m1  10391  frec2uz0d  10724  frec2uzzd  10725  frec2uzsucd  10726  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdg0  10738  frecuzrdgsuc  10739  frecuzrdgg  10741  frecuzrdg0t  10747  frecuzrdgsuctlem  10748  0tonninf  10765  1tonninf  10766  inftonninf  10767  seq3val  10785  seqvalcd  10786  hashinfom  11103  hashennn  11105  hashfz1  11108  ccat1st1st  11284  cats1fvd  11413  shftidt  11473  resqrexlemf1  11648  resqrexlemfp1  11649  cbvsum  12000  fisumss  12033  fsumadd  12047  isumclim3  12064  cbvprod  12199  fprodssdc  12231  nninfctlemfo  12691  ialgr0  12696  algrp1  12698  ennnfonelem0  13106  ennnfonelemp1  13107  ennnfonelemom  13109  ctinfomlemom  13128  nninfdclemp1  13151  ndxarg  13185  strslfv2d  13205  prdsidlem  13610  prdsinvlem  13771  ringidvalg  14055  lidlvalg  14567  rspvalg  14568  znf1o  14747  mplnegfi  14806  upxp  15083  cnmetdval  15340  remetdval  15358  reeflog  15674  ushgredgedg  16167  ushgredgedgloop  16169  subgruhgredgdm  16211  vtxdumgrfival  16239  vtxd0nedgbfi  16240  vtxduspgrfvedgfi  16242  wlk1walkdom  16300  wlkres  16320  depindlem1  16447  nninfnfiinf  16749